Speculation by Default: A Verified Proposal, a Graded Dossier and a Single Commit Between Running Composition and Disk

Pitch

An agent's edit is verified on a per-caller proposal and, on the speculative path, only one explicit commit, re-verified against the live composition, can change what runs or what is on disk, and undo is a recompile through the same gate.

Abstract

LLM coding agents usually edit by mutating: the tool applies the patch, then a test run or a human finds out whether it was acceptable, and "undo" is a second mutation that nobody checks. We describe the edit loop of revl's agent session, built around three states: the running composition with the exact source it was compiled from (shared by every caller), a per-caller proposal (a speculative working copy), and disk (an export, written only by one verb). A change is applied to the proposal and run through the same admission, lease and quarantine gates a live swap would face, optionally followed by a gauntlet that grades the candidate in an isolated scratch session and returns a dossier separating what was proved, what was tested with counts and what is merely claimed. On the speculative path nothing swaps or writes until an explicit commit, which re-verifies against the composition as it is now and is refused if another caller committed in between, rather than silently undoing that commit. Undo recompiles the target generation's sources through the compile and admission gate, so a generation a stricter checker now rejects cannot be restored by backdoor. A repair loop composes these pieces (fault, causal trace, bisect, candidate, gauntlet, policy, widening check, swap) and is exercised by an unattended end-to-end test. We report what is shipped: 12 speculation tests, a stale-proposal refusal test and an undo-refuses-rejected-target test. We also report the gaps the design doc itself names: revl_edit still commits by default, the quarantine and lease gates do not cover undo, two dossier slots are hard-coded pending, and the repair loop does not yet use the canary.

Problem and claim

Agent tools put "try this" and "do this" in the same call. The design doc states it directly: the loop an agent runs still mutates on the first step (docs/design/1696-speculation.md:5-11). A rejected-after-the-fact edit has already been seen by every other client, and the only durable form of the work is a file the agent writes outside the system. Undo, where it exists, is often another unchecked mutation (citation to be checked, product docs).

The claim is about the structure of the loop, not about model quality: (a) a speculative change never swaps and never writes; (b) a commit is the only state change another caller can observe; (c) a commit verifies again, and refuses if the running generation moved; (d) export writes exactly the held source (docs/design/1696-speculation.md:64-75). Together with undo being a gated recompile (docs/generation-history.md:46-65), this leaves one admission gate that every swap path reaches, the compile and admission gate, instead of one verification design per verb. Quarantine and lease are not on every path (see below).

The claim has a precise boundary, and the paper should state it. "No mutation path bypasses verification" holds for the admission gate: a swap, an edit commit, an undo and a repair all reach it. It does not hold for every gate: docs/quarantine-tier.md:112-115 says undo and rollback reach the swap with neither the quarantine gate nor the lease check. And the default of the most-used verb is not speculative yet (see Evidence).

Contributions

1. A three-state model (running composition with held source; per-caller proposal keyed by operator identity; disk as export) with stale-proposal refusal in place of silent overwrite (src/revl/mcp/proposal.py:1-18, src/revl/mcp/proposal.py:71-79; docs/design/1696-speculation.md:13-38).
2. A speculative-by-default change verb (revl_change) whose proposal runs the full verification and then stops, with commit and discard as the only exits (src/revl/mcp/server.py:1744; docs/design/1696-speculation.md:40-62).
3. Undo as a gated change: the target generation's sources are recompiled through the same gate as a swap, a rejected target is a refusal result with the composition untouched, and every successful mutating response carries its undo call, or undo: null with a reason (docs/generation-history.md:46-90; src/revl/mcp/session.py:2937-3010; tests/test_undo.py:230).
4. A graded candidate dossier, revl_gauntlet, run in a throwaway scratch session, with an explicit epistemic split into proved, tested (with counts) and claimed (docs/gauntlet.md:17-35, docs/gauntlet.md:115-125; tests/test_gauntlet.py:191).
5. A quarantine tier whose verdicts (passed, trapped, timeout, rejected, deferred, unavailable) come from running the candidate under a wasm component runtime, with an admission hook that applies only where policy requires it (docs/quarantine-tier.md:74-116).
6. A repair loop that composes the above with a closed-by-default self-repair policy and a human-ack interrupt on widened reach, with an unattended exit test (docs/repair-loop.md:19-110, docs/repair-loop.md:179-188; tests/test_repair_loop.py:234).

Related work

Evidence on main

Numbers that exist

• Test counts by rg -c "^def test" on the tree (not run for this draft): speculation 12, gauntlet 9, quarantine 20, repair loop 16, apply 13, undo 12, mcp undo 15, canary 15.
• Generation history is bounded: HISTORY_LIMIT 64 (src/revl/mcp/session.py:390; docs/generation-history.md:30-33).
• The gauntlet lifecycle example in the doc shows checks: 5, passed: 5 as a schema illustration, not a measured result (docs/gauntlet.md:65-70).
• No measurements on real agents: no task success rate, no regression-catch rate, no latency of the speculative path, no comparison against apply-then-test.

Paper outline

1. Introduction: "try" and "do" are the same call; the claim and its boundary.
2. The three states, the proposal, the commit; guarantees (a) to (d).
3. Verification stages: admission, lease, quarantine, gauntlet; what each can and cannot show.
4. Undo as a gated change; the undo contract on every mutating response; where undo is deliberately weaker.
5. The graded dossier: proved, tested, claimed; isolation of the scratch session.
6. Composition: the repair loop and its closed-by-default policy.
7. Evaluation: verify-before-commit against apply-then-test on seeded defects, a multi-caller overwrite count, repair-loop outcomes.
8. Limits and open gaps (edit default, undo exceptions, pending slots).
9. Related work and conclusion.

Threats to validity and limits

• The thesis "no mutation path bypasses verification" is stronger than the code: undo and rollback bypass the quarantine and lease gates by documented design (docs/quarantine-tier.md:112-115), and revl_edit commits by default (src/revl/mcp/server.py:2136).
• The gauntlet isolates a candidate from the live composition, not from the host: host-body externs run in the server's process; the docs call isolation "not a licence to run what the gate refuses" (docs/gauntlet.md:127-137). The wasm substrate is what confines, and only where the toolchain exists and the candidate's boundary types lower (Float, Map, resource handles and function values are deferred, docs/quarantine-tier.md:158-164).
• The "claimed" section lists the extern boundary rather than checking it. The dossier shape is stable, but two of the three evidence kinds that would shrink "claimed" are not wired.
• A speculative undo guarantee is byte-for-byte on sources and manifest only; running state is not part of that promise (docs/generation-history.md:73-74).
• revl apply verifies a plan against its own predicted outcome (docs/apply.md:127-130).
• Per-caller proposals are keyed by operator identity on one server; this is not a distributed system and the paper should not claim it.
• All current evidence is tests written by the project team; there is no study with external agents or users.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 20 checked, 6 corrected.

Cite this draft

@misc{revlp22,
  author       = {Thomas Moussajee},
  title        = {Speculation by Default: A Verified Proposal, a Graded Dossier and a Single Commit Between Running Composition and Disk},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P22.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.