diff --git a/README.md b/README.md
index 1e66078..7c1c35b 100644
--- a/README.md
+++ b/README.md
@@ -9,8 +9,9 @@
 - **Line-level merging:** agents editing different lines of one file both get in.
 - **Conflicts are data:** overlapping edits stay side by side until a reviewed resolution patch.
 - **Enforced review:** admission needs an independent approval and a passing check.
-- **Verified core:** every registry decision is extracted Rust, proved in Lean.
+- **Verified core:** the Rust kernels that admit patches and merge files are translated to Lean by Aeneas, and their guarantees are proved about that translation.
 - **Plain Git at the edges:** agents work in ordinary checkouts; snapshots export to Git.
+- **Runs on Cloudflare:** a Rust Worker serves the same API over PostgreSQL (Hyperdrive); Git exports and agent workspaces live in Cloudflare Artifacts, re-delivered by a Cron Trigger.
 
 ```bash
 ./scripts/dev.sh                              # Start a local server; prints three tokens