● OPERATOR OF RECORD · MICHAEL MOFFETT · accountable on every commit team@caliperforge.com
BLOG · 2026-07-14 · MICHAEL MOFFETT

The reachability certification: sixteen seeds, hard alarm.

We publish clean/planted twin repositories for recurring bug classes in on-chain protocol code. The pattern is: for a fixed bug class in a specific protocol commit, vendor the protocol source at the fix commit, encode the invariant that the fix defends, and ship two twins. A clean twin that holds the invariant on every fuzzed sequence, and a planted twin whose only diff is a single-hunk revert of the fix. Wire both twins as required CI jobs. Invert the planted job so its "success" means the property test failed loudly on the planted twin. That combination is the standing receipt: on every commit, the invariant catches the class it claims to catch.

This week, an external reviewer looked at that shape and pointed out a real gap. The planted twin only fails when the fuzzer's random walk actually reaches the trigger sequence within one bounded campaign. For short triggers (the two-step call sequence in Euler Earn's M-01, for instance) that is not much of a gap: any reasonable seed reaches the trigger. For longer or rarer trigger sequences, "the planted twin failed the invariant on the CI run" is probabilistic evidence, not proof. A run that happens to draw a lucky seed can look green and mean nothing. The headline framing "standing proof the property catches the class" was probabilistic in exactly that spot.

The fix is straightforward and we shipped it the same day. This post is the walk-through.

The seed-reliability problem

The seed-reliability problem.

Property-based fuzzers (Foundry's forge test --fuzz-seed, Rust proptest's TestRunner::new_with_rng) draw pseudo-random operation sequences. Given the same seed, the same source, and the same toolchain, they draw the same sequences. Different seeds draw different sequences. A campaign at budget 256 runs times depth 50 covers a lot of state space, but the covered slice is a function of the seed.

If a class's trigger is short, say a two-step directShareDeposit then reallocateFromStrategy in the Euler Earn M-01 case, nearly every reasonable seed will draw a sequence that touches the trigger inside a 256-by-50 campaign, and the planted twin will fail loudly. The receipt is a receipt.

If a class's trigger is long, or a specific ordering of a large set of operations, or a rare combination of parameter values, one seed might draw a sequence that fires the marker while another seed draws a sequence that never touches the trigger and passes the planted twin quietly. That last case is a false green: the receipt claims a hard alarm on the class, and the run says PASS on the planted twin. The receipt has degraded silently.

The scale of the gap depends on the class. For our first two publicly-critiqued cases (Euler Earn M-01 and Blend V2 H-01), we did not have a rigorous claim about how many seeds would consistently fire the planted twin. "It failed on the CI seed we happened to use" was what we could say. The reviewer read the docs, saw the shape, and named the gap. Fair reading.

The 16-seed fail-on-all gate

The 16-seed fail-on-all gate.

The fix is a merge gate. A case is certified reachable if, and only if, the planted twin fails the invariant on all N distinct fuzzer seeds in a canonical seed set. The canonical seed set lives at ci/reachability_seeds.txt in each case repo (identical file across repos) and contains N=16 distinct u64 values: a mix of small integers, common testing patterns (0xdeadbeef, 0xcafebabe, 0xfeedface, 0x1337c0de), and pseudo-random bytes. Fixed list, order-stable, not RNG-derived.

Each case repo carries a ci/reachability_leg.sh runner tuned to the case's toolchain. On the Euler M-01 case (Foundry), the runner loops the seed set, invokes forge test --match-contract M01SolvencyPlanted --fuzz-seed <seed>, records per-seed rc plus INVARIANT VIOLATED marker count, and emits one verdict line: reachability certified: yes (k/N failed as required) or no. On the Soroban Blend V2 H-01 case (Rust / proptest), the runner exports REACHABILITY_SEED and runs cargo test -p <planted-crate> --test reachability -- --nocapture. The Rust test file tests/reachability.rs parses the env var, tiles the 8-byte value to a 32-byte ChaCha seed, and constructs TestRunner::new_with_rng(config, TestRng::from_seed(RngAlgorithm::ChaCha, &seed)). No fallback to a default seed, no time-of-day input, deterministic given seed plus source plus toolchain.

Each case repo carries a CI-leg script that runs the same 16-seed loop as an additional parallel CI job. In caliperforge/euler-earn-invariants, the job is reachability-multi-seed, running alongside the existing clean-passes and planted-bug-twin-fails jobs. In caliperforge/soroban-invariant-atlas, the job is reachability, running alongside clean, planted, fmt, and clippy. The pre-existing clean-green / planted-red inversion is unchanged; the new job adds a merge gate that requires the planted twin to fail all 16 seeds on repo HEAD.

The merge-gate rule is one line in each case's docs/reachability.md: no case merges to main unless the multi-seed reachability job is green on the head commit. Future case authors extending the pattern lift the same script and seed set verbatim.

What the two certifications look like today

What the two certifications look like today.

Two cases certified as of today:

Euler Earn M-01 (Foundry). Repo: caliperforge/euler-earn-invariants. Head commit 8696baf add multi-seed reachability gate (M-01 planted twin). CI run 29269639472. All three parallel jobs green. Certification line in README and docs/reachability.md: reachability certified: yes (16/16 failed as required) (2026-07-13).

Blend V2 H-01 (Rust / Soroban). Repo: caliperforge/soroban-invariant-atlas, case blendv2-h01. Head commit d4e9164 add multi-seed reachability gate (case C-A1 Blend V2 H-01). CI run 29269645178. All five parallel jobs green (clean, planted, fmt, clippy, reachability). Certification line in README, docs/reachability.md, and cases/blendv2-h01/README.md: reachability certified: yes (16/16 failed as required) (2026-07-13).

Both certifications hold at the case's current campaign budget. Foundry runs at 256 runs times depth 50 per foundry.toml; the Soroban proptest campaign runs at 256 cases with sequence length up to 24. If a future case cannot certify at the case's base budget, the merge-gate rule is explicit about two honest branches: bump the budget until the case certifies, or document the achieved k/N caveat in the case README and refuse to claim certified: yes in the docs.

What this changes about the framing

What this changes about the framing.

Before this week, the receipt line under a planted twin was "the property test caught the class." Load-bearing but probabilistic under one seed. The reviewer's reading was correct: a green CI run with one seed does not exclude the possibility of a lucky seed on a class with a rare trigger. The framing was stronger than the underlying evidence.

After this week, the receipt line under a certified case is "the planted twin fails on all 16 canonical fuzzer seeds." Bounded, precise, and cited to the seed set + the CI run + the docs verdict. It is a hard alarm, not a lucky green.

The framing change is what we owe the reader. It also happens to be exactly what a class-encoded CI receipt should look like: name N, run against N, publish the k/N, and refuse to claim "certified" if k does not equal N.

What I am not claiming

What I am not claiming.

I am not claiming 16 seeds is universally sufficient. It is a canonical set that reliably breaks the "lucky single-seed" reading of a green planted-twin CI run for the classes we have certified today. For a class with a genuinely rare trigger, 16 seeds is a floor, not a ceiling; the honest branch is bumping the budget until certified, or documenting the caveat. The rule allows both.

I am not claiming the reachability gate replaces a formal proof. It does not. A stateful fuzzer campaign, even seeded 16 different ways, is a runnable receipt against a bounded search of the state space. Formal verification is a different tool with different guarantees; the clean/planted twin pair is a defender-side regression fixture, not a soundness certificate.

I am not claiming this method is novel or that no other harness runs a multi-seed pattern. Seed rotation is standard fuzzing hygiene; property-based testing suites have supported it for years. What we added is a merge gate that ties the standing "certified" claim in the docs to the concrete 16-seed pass on the CI, so the docs cannot drift from the receipt.

Where the receipt lives

Where the receipt lives.

Credit for the critique

Credit for the critique.

The critique that motivated the gate came from an external reviewer, Aminu Abubakar (handle aegonmyy). We name it because reviewer credit is the discipline: name the reader who improved the work, cite the shape of the improvement, and ship the fix. The reviewer named a probabilistic gap in a claim that read as deterministic; the fix is the multi-seed gate above.

This writeup was drafted with AI assistance. Authored and reviewed by Michael Moffett, operator at CaliperForge. Full policy at caliperforge.com/ai-disclosure.