From 54a0cbd08e0e5d5940de86ac586c434d4efcc455 Mon Sep 17 00:00:00 2001 From: koukyosyumei Date: Tue, 13 Oct 2026 09:28:07 -0400 Subject: [PATCH 1/2] README: how o5s uses Workers and Artifacts --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 1e66078..4fa4cd5 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,7 @@ - **Enforced review:** admission needs an independent approval and a passing check. - **Verified core:** every registry decision is extracted Rust, proved in Lean. - **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 From cbf6a14c8cda173af4ab0f99953f2b185b6367c5 Mon Sep 17 00:00:00 2001 From: koukyosyumei Date: Tue, 13 Oct 2026 09:35:31 -0400 Subject: [PATCH 2/2] README: say what the verified core is --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4fa4cd5..7c1c35b 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ - **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.