diff --git a/examples/guide/async_await.rs b/examples/guide/async_await.rs
new file mode 100644
index 0000000000..9121c25707
--- /dev/null
+++ b/examples/guide/async_await.rs
@@ -0,0 +1,88 @@
+#[allow(unused_imports)]
+use verus_builtin::*;
+#[allow(unused_imports)]
+use verus_builtin_macros::*;
+#[allow(unused_imports)]
+use vstd::seq::*;
+
+verus! {
+
+// ANCHOR: basic_async_ensures
+async fn add1(x: u64) -> (result: u64)
+    requires x < u64::MAX,
+    ensures result == x + 1,
+{
+    x + 1
+}
+// ANCHOR_END: basic_async_ensures
+
+// ANCHOR: basic_async_caller
+async fn async_call(x: u64)
+{
+    let result = add1(41).await;
+    assert(result == 42);
+    let future = add1(41);
+    // ^ This future has not yet executed, so the following
+    // assertion would fail; the value of a future can be obtained
+    // via `.view()` or `@`.
+
+    // assert(future@ == 42);
+}
+// ANCHOR_END: basic_async_caller
+
+// ANCHOR: basic_async_caller_awaited
+use vstd::future::FutureAdditionalSpecFns;
+async fn async_call2(x: u64)
+{
+    let future = add1(41);
+    assert(future.awaited() ==> future@ == 42);
+    future.await;
+    assert(future.awaited());
+}
+// ANCHOR_END: basic_async_caller_awaited
+
+// ANCHOR: async_future_branch
+use std::future::Future;
+async fn branch_and_await<T>(
+    run_first: bool,
+    f1: impl Future<Output = T>,
+    f2: impl Future<Output = T>,
+) -> (result: T)
+    ensures
+        run_first ==> f1.awaited() && result == f1@,
+        !run_first ==> f2.awaited() && result == f2@,
+{
+    if run_first {
+        f1.await
+    } else {
+        f2.await
+    }
+}
+
+async fn call_branch() {
+    let f1 = add1(22);
+    let f2 = add1(41);
+    let result = branch_and_await(true, f1, f2).await;
+    assert(result == 23 && f1.awaited());
+}
+// ANCHOR_END: async_future_branch
+
+// ANCHOR: async_mut
+async fn mutating_arg(x: &mut usize) -> (result: ())
+    requires *old(x) < usize::MAX,
+    ensures *x == *old(x) + 1
+{
+    *x += 1;
+}
+
+async fn using_async_mutation() {
+    let mut x = 42;
+    let f = mutating_arg(&mut x);
+    // assert(x == 42); // should fail
+    // assert(x == 43); // should fail
+    f.await;
+    assert(x == 43);
+}
+// ANCHOR_END: async_mut
+
+}
\ No newline at end of file
diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index 578e010fa5..8d42c7b858 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -107,6 +107,8 @@
   - [Memory safety is conditional on verification](./memory-safety.md)
   - [Calling verified code from unverified code](./call-from-unverified-code.md)
 
+- [Verifying asynchronous code](./async-await.md)
+
 # Installation, configuration, and tooling
 
 - [Installation and setup]()
diff --git a/source/docs/guide/src/async-await.md b/source/docs/guide/src/async-await.md
new file mode 100644
index 0000000000..52612b185c
--- /dev/null
+++ b/source/docs/guide/src/async-await.md
@@ -0,0 +1,110 @@
+# Verifying asynchronous code
+
+Rust supports writing asynchronous code without manually managing which thread a
+given task is performed on using the `async` and `await` keywords. This
+functionality is often useful for managing multiple IO-bound tasks. [This Rust
+book chapter](https://doc.rust-lang.org/book/ch17-00-async-await.html) contains
+a detailed introduction to this feature.
+
+## Basics
+
+Verus supports reasoning about code using `async`/`await`. Just
+like regular `fn`s, `async fn`s can be annotated with `requires`
+and `ensures` clauses:
+
+```rust
+{{#include ../../../../examples/guide/async_await.rs:basic_async_ensures}}
+```
+
+`result` in the `ensure`s clause refers to the value of the future,
+once it has completed. At a call site of `add1`, the postcondition
+is only known to hold once the future is awaited:
+
+```rust
+{{#include ../../../../examples/guide/async_await.rs:basic_async_caller}}
+```
+
+`assert(future@ == 42)` fails because the postcondition of an
+unawaited future is guarded by an uninterpreted `.awaited()` predicate
+that is known to be true only if a future has been awaited.
+
+```rust
+{{#include ../../../../examples/guide/async_await.rs:basic_async_caller_awaited}}
+```
+
+Assertions about futures that have not yet been awaited are often useful when
+writing functions that consume other futures as input; for example, consider
+the function `branch_and_await` that conditionally awaits only
+one of its arguments.
+
+```rust
+{{#include ../../../../examples/guide/async_await.rs:basic_async_future_branch}}
+```
+
+## Mutability
+
+`async fn`s can also take mutable references as arguments and change their
+values. The mutations are only known to have taken effect once the future
+has been awaited.
+
+```rust
+{{#include ../../../../examples/guide/async_await.rs:async_mut}}
+```
+
+*Note*: Technically, Rust guarantees that after creating, but not `await`ing,
+`f`, `*x` will still have value `42`. However, to avoid complex tracking of when
+a future may have started executing, Verus treats this imprecisely and considers
+`x` to have an unknown value as soon as it is passed to `mutating_arg`, until
+the resulting future is `await`ed. Please create an issue if you have a use case
+where knowing that a future has not yet started to execute is important.
+
+## Using libraries
+
+`async`/`await` is frequently used with supporting libraries such as
+[tokio](https://tokio.rs/) that provide a runtime support to execute
+asynchronous code, as well as additional primitives. For example, `tokio`s
+`select!` macro allows racing multiple futures and acting on the first future
+that completes. Note that the examples below require the `macros` feature of the
+`tokio` dependency to be enabled. To verify the examples, run `cargo add tokio -F macros`
+in your project once, and then use `cargo verus verify` instead of plain Verus invocations.
+
+```rust
+select! {
+    add1(42) = r1 => r1,
+    add1(21) = r2 => r2,
+}
+```
+
+This code runs both futures `add1(42)` and `add1(21)` concurrently and returns
+the value of whichever completes first; the syntax `expr = var => ret` binds
+the value `expr` completed with to `var` and executes expression `ret`.
+
+While `verus` does not natively understand how to reason about the code
+generated by the `select!` macro, we can use mechanisms for specifying
+assumptions on external code, such as `#[verifier::external_body]` for
+specific uses of `select!`:
+
+```rust
+#[verifier::external_body]
+async fn race_futures<T>(f1: impl Future<Output = T>, f2: impl Future<Output = T>) -> (res: T)
+    ensures
+        (f1.awaited() && res == f1@) || (f2.awaited() && res == f2@),
+{
+    tokio::select! {
+        a = f1 => a,
+        b = f2 => b,
+    }
+}
+```
+
+The above postcondition is *trusted*! Verus does not check that the body in fact
+guarantees the postcondition. It states that after `race_futures` completes, one
+of the two input futures will have been awaited and its result returned. This
+can then be used in callers:
+
+```rust
+let f1 = add(3, 5);
+let f2 = add(7, 5);
+let result: usize = race_futures(f1, f2).await ;
+assert(result <= 12);
+```
\ No newline at end of file
diff --git a/source/docs/guide/src/features.md b/source/docs/guide/src/features.md
index 1948b3c772..8a80bc8269 100644
--- a/source/docs/guide/src/features.md
+++ b/source/docs/guide/src/features.md
@@ -4,7 +4,7 @@ Quick reference for supported Rust features. Note that this list does not includ
 
 Note that Verus is in active development. If a feature is unsupported, it might be genuinely hard, or it might just be low priority. See the [github issues](https://github.com/verus-lang/verus/issues) or [discussions](https://github.com/verus-lang/verus/discussions) for information on planned features.
 
-**Last Updated: 2026-02-18**
+**Last Updated: 2026-04-13**
 
 <div class="table-wrapper"><table>
   <thead><tr><th colspan="2"><strong>Items</strong></th></tr></thead>
@@ -31,7 +31,7 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td>Async functions</td>
-    <td>Not supported</td>
+    <td>Supported</td>
   </tr>
   <tr>
     <td>Macros</td>
@@ -267,7 +267,7 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td>impl types</td>
-    <td>Partially supported</td>
+    <td>Supported</td>
   </tr>
   <tr>
     <td>Cell, RefCell</td>