Read the proof, then read the claim.
A green-looking page is not the verification system. Tasks move to
verified only after a fresh verifier interrogates recorded evidence against
the diff. This page is the short version of that contract and the current status that
follows from it.
The worker/verifier loop
The worker's summary is a claim. The evidence is the replayable record: deterministic command output, guest traces and digests, browser assertions, and rr or rr-soft when the host-layer risk requires it. A verifier also audits changed lines for coverage. An unexecuted behavior is a proof gap, not a green check.
What the repository has recorded
| Boundary | Recorded result | Read the full record |
|---|---|---|
| Level 1 architecture | 395 RISCOF cases passed, 0 failed, and no exclusions in the frozen report; native/WASM equality is part of the gate. | Level 1 report |
| Release boundary | The named v0.1 boundary is the verified Epic 3 capstone plus the Level 1 and Level 2 foundations. Later acceleration, GUI, SMP, and sharing work is outside that claim. | Release assurance |
| Browser compliance record | Recent exact-head evidence records a browser compliance run at 126 passed / 0 failed with zero console errors for that tested build. | E4-T33 evidence log |
| OCI container path | The image matrix and runner sub-capstones have evidence, while the full boot-gated container capstone remains separately tracked. | Container page |
Current status that matters
verified Architecture and core browser boundary
Use the Level 1 report and generated wasm declarations for the claims that are actually frozen and replayed.
in progress E4-T34 short-block JIT
The task still requires the real restored Node workload, wall-time thresholds, boundary-rate improvement, and adversarial exactness. The retrospective explicitly does not claim completion.
pending Boot-gated container capstone
Static image validation is not the same as booting every image and watching its service run inside the emulator.
proposal ProofMesh product layer
Product, market, encrypted-volume, and distributed-delivery pages describe roadmap contracts, not current VM APIs.
Local gates
This repository's operating manual keeps verification local and deploys the static web output to Cloudflare Pages. Run the narrowest affected gate while iterating, then the risk-tier submission at the frozen head.
cargo fmt --all -- --check
cargo clippy --workspace --all-targets --all-features -- -D warnings
cargo test --workspace
make web-build
make web-dist
bash tools/deploy-cloudflare.shBrowser-facing changes also need a built-page assertion: load the generated page, check the affected behavior, check console errors, and record the result. The public deploy is not proof by itself; it is the artifact that must match the evidence.
Host-layer evidence. macOS can provide native tests and guest/browser
evidence, but rr is a Linux tool. The repository's rr-soft workflow uses
ssh dev for replayable host traces when a high-risk task needs them. This
docs rewrite does not change runtime behavior or require a new rr recording.
Source records
AGENTS.md— roles, evidence doctrine, risk tiers, and deployment rules.tasks/— authoritative per-task status and verification logs.docs/perf/e4-t34-jit-retrospective.md— why the JIT speedup claim remains open.tasks/QUEUE.md— generated queue view.