What runs today.
What comes next.

• Persistent handoff of citations, assessments and artifacts between the tools
• Approved worktree edits replayed through the pinned Splicery kernel
• Recovery after a crash, when the outcome of an edit is unknown
• Session benchmarks with retained evidence

The trial profile now retains citations, binds Weft reports, and approves, applies and recovers edits within its own cooperating scope. These scenarios stay blocked until the hardened services run them.

Trust base for the proofs: the Charon/Aeneas translation, the Aeneas library's models of the Rust operations used, the Lean kernel and Lean's standard axioms. Everything outside those kernels is tested, not proved, and the kernel specifications are not yet machine-linked to the calculus. How we know lists each kernel.

Correctness was equal in both pilots, and the Writfold flow cost about 16% more tokens: there is no token win yet. What it adds is structural: the agent never wrote the checkout, and every applied edit carries a verified approval and a recorded outcome. In one task the agent’s first preparation would have joined two lines; it was never approved, a corrected one was applied, and the rejected one never touched a file. In these pilots the agent approved its own edits, so they measure mechanics and overhead, not human review; approval has since become CLI-only for serve sessions.

The projection pilot compared Tuft with grep-and-read on six evidence-finding tasks (two repeats each, same model). Correctness was 12/12 in both arms, and the Tuft arm used 5.3% more tokens, more on every task. The tasks had 1 to 9 matches, so Tuft's budget and omissions never came into play. Agents also retyped Tuft's quoted rows by hand where grep output could be piped, and Tuft's headers and byte ranges roughly doubled the tool output. A second projection pilot used lean compact output and tasks with up to 297 matching lines: correctness was again 12/12 in both arms, and the Tuft arm used 3.1% more tokens, more on all six tasks. Its tool output was 5.6% smaller, but agents wrote longer programs and made more calls, and grep pipelines already kept the other arm's output small. So Tuft's typed output costs about the same as grep: within 3.1% of grep's tokens, Tuft gives search pinned to one commit, a completeness signal (coverage, omissions, cursor) and retained citations a Weft report and an approval can bind to. It does not save tokens on lookups a shell pipeline can reduce. Raw data: projection pilot 2, projection pilot, trial-flow pilot, edit pilot.

Done in the trial profile: a durable, validated ledger with grants; retain, prepare, approve, apply and recover through the CLI; show, retain, prepare, run and evidence reads through serve; Tuft v0; evidence reuse across sessions; a Dolt writer with a first publication path. Not built: semantic or fuzzy search, a live knowledge service, named contexts and receipts beyond the trial ledger.

1. Fewer agent mistakes, measured

   Harder reliability tasks (an unfamiliar repository, multi-file edits, a file changed between prepare and apply), and trial state found without an environment variable, the main trip in the first pilot.

2. Publication

   A signed candidate binding, first publication into an empty realm, and a TLA+ model of the publication order, with its decision code proved.

3. Storage

   Omnigraph behind the same boundary once it is admitted.

1. 10 Nov 2026

   serve now runs the one-command trial run and reads retained evidence (trial/run, trial/evidence-list, trial/evidence-show), as a revision of writfold.trial/1; the Weft binary is fixed when the server starts, never named by the client, and approval stays CLI-only. Dolt publication, first slice: one signed approval publishes one candidate; Dolt commits first and moving the Git release ref is the only point it becomes visible, so a crash leaves an interrupted publication that is completed with Git steps only. A kill sweep against real Dolt ended with no double publication and found two crash bugs, both fixed. Tuft's resume cursor is now typed and bound to its program, commit and rows. A first reliability pilot measured mistakes instead of tokens, with a smaller model: 23 of 24 clean trials with ordinary tools, 24 of 24 with Writfold and Tuft, too close to tell apart; the tasks were too easy.

2. 10 Nov 2026

   One command, writfold trial run, goes from a Tuft query through a Weft check to a prepared edit and stops at approval. writfold trial evidence list and show read retained evidence back in a later session, verified against its digest. Dolt, the interim backend, gained a conditional single writer: one transaction guarded by the expected head, an exclusive writer lease and a signed approval; an interrupted write is Unknown and never retried, and passed a kill sweep against real Dolt. The trial's edit-flow validator is now proved over the shipped Rust, and a TLA+ model of the trial stream (crashes, recovery and an outside writer) checks with no violation while two deliberately broken variants are caught. Tuft got its own page, compact output and two more pilots.

3. 9 Nov 2026

   Source-only preview v0.1.0-dev.1: a cooperating single-user trial that runs end to end, with its commands reproduced from a fresh clone. New: trial retain keeps exact bytes as citations; Tuft v0 finds, retains and projects exact evidence over a pinned commit; a Weft report is bound at prepare and approve --require refuses unless named checks are entailed; trial show prints five independent badges; serve exposes show, retain and prepare, with approval CLI-only. Proved over the shipped Rust: revocation, the recovery outcome and the required-check gate; 20 of 20 semantic mutants rejected. An adversarial campaign ended as expected in 8 of 8 cases, including 60 random SIGKILLs during apply. A sparse worktree cut prepare on a 100,000-file repository from 7,772 ms to a p95 of 239 ms. Dolt became the interim backend behind a swappable storage boundary; Omnigraph remains the target, and Dolt writes are not built.

4. 9 Nov 2026

   Decision kernels proved over the shipped Rust with Charon/Aeneas and Lean 4: Writfold's ledger and grant authority (51 theorems), Weft's set algebra, verdict classification and reuse comparison, and Splicery's edit rendering. Every deliberately broken copy of each kernel breaks its named theorem. The proofs found and fixed an integer-overflow edge in the ledger's sequence check. Splicery's Verus proofs for that kernel were retired in favour of these.

5. 9 Nov 2026

   First connected flow: writfold trial prepares a Splicery edit in Writfold’s own worktree of any Git repository, signs a grant and approval, and applies the edit only after re-verifying them and the file. Every step is recorded in a durable, kernel-validated ledger stored in Git. A cooperating single-user trial profile, not the hardened path.

6. 8 Nov 2026

   Repositories made public. First agent edit pilot published, with no measured win yet. Signed operator grants and revocations, and a current-grant check that agrees with the Lean model on 79 exported steps. Signed approval of one exact prepared edit; a validated ledger that replays full history before each conditional append; procedure checking and the ledger now checked against cases exported from the Lean model. Also tested as separate parts: exact object storage, Git worktree creation and ledger-head decoding. Weft accepts large prior reports for reuse.

7. 7 Nov 2026

   Rust Omnigraph data path tested. A source build of Omnigraph PR #1235 passed the scoped relocation and restore test. Scope of the first experimental release agreed.

8. 6 Nov 2026

   Writfold, Weft and Splicery exercised together: 12 scenarios across 29 invocations.

9. 5 Nov 2026

   writfold serve stdio session, citation components and dependency locks.

10. 4 Nov 2026

    The twelve engineering theorems proved in Lean under stated assumptions.

11. 2 Nov 2026

    Semantic core ported to Rust; static Linux builds.

12. 1 Nov 2026

    Writfold started as the Rust successor to an earlier private prototype.

Every published file on this site is listed with its SHA-256 in the content manifest.