A cross-repo survey of the toolchain's test surface found scry is the only repo with neither fuzz targets nor property tests, while it is the component whose central claim is soundness.
Evidence (as of this filing)
| repo |
fuzz targets |
proptest/quickcheck |
| synth |
49 files |
35 crates |
| rivet |
40 files |
4 crates (28 files) |
| kiln |
14 files (3 dirs) |
5 crates |
| sigil |
10 files |
— |
| spar |
6 files |
3 crates |
| meld |
4 files |
2 crates |
| loom |
3 files |
2 crates |
| relay |
2 files |
36 crates (41 files) |
| scry |
0 |
0 |
Six repos additionally wire fuzzing into CI (fuzz.yml, fuzz-smoke.yml, fuzz-nightly.yml). scry's workflows are ci.yml, rocq-proofs.yml, verus-proofs.yml, rivet-delta.yml, publish/release — no fuzz job.
Why this matters specifically for scry
scry has 14 crates and parses WebAssembly (scry-analyze-core, scry-provenance). Its mechanized proofs (proofs/rocq/Soundness.v, WrapAdd.v) establish soundness of the abstract domain — the interval lattice, the transfer functions, i32.add against official wrapping semantics. They say nothing about the frontend: the path from untrusted bytes → parsed module → the analysis those proofs are about.
That is the toolchain's recurring fault class, applied to scry: a guarantee that is not enforced on the path that executes. A sound analyzer that panics, hangs, or mis-parses a malformed/adversarial module has not violated its soundness theorem — it has bypassed it. For a DO-333-positioned tool, "the analyzer crashed on the input" and "the analyzer silently analyzed something other than the shipped module" are both qualification-relevant.
Suggested scope
- Fuzz the frontend —
cargo-fuzz target over the module parser / analysis entry point; corpus seeded from the existing test wasm + the toolchain's bench modules. Kill-criterion: no panic, no unbounded run, on any input.
- Property-test the domain — proptest over the interval/float/octagon lattices for the algebraic laws the Rocq proofs assume the Rust implementation satisfies (join/meet commutativity + associativity, monotonicity, γ-concretization containment). This is the cheap mechanical dual of the proofs: the proofs say the model is sound; proptest checks the shipped Rust obeys the same laws.
- Wire it in CI — a
fuzz.yml matching the pattern already used by rivet/loom/meld/sigil (smoke on PR, longer nightly).
Item 2 is arguably the higher-value half: it closes the model↔implementation gap that a proof alone leaves open.
Not a soundness accusation
No mis-analysis is being reported here — this is a missing guard, found by surveying test surfaces across repos, not by observing a failure. Filing so the gap is explicit rather than implicit.
🤖 Filed via Claude Code from a cross-repo test-surface survey.
A cross-repo survey of the toolchain's test surface found scry is the only repo with neither fuzz targets nor property tests, while it is the component whose central claim is soundness.
Evidence (as of this filing)
Six repos additionally wire fuzzing into CI (
fuzz.yml,fuzz-smoke.yml,fuzz-nightly.yml). scry's workflows areci.yml,rocq-proofs.yml,verus-proofs.yml,rivet-delta.yml, publish/release — no fuzz job.Why this matters specifically for scry
scry has 14 crates and parses WebAssembly (
scry-analyze-core,scry-provenance). Its mechanized proofs (proofs/rocq/Soundness.v,WrapAdd.v) establish soundness of the abstract domain — the interval lattice, the transfer functions,i32.addagainst official wrapping semantics. They say nothing about the frontend: the path from untrusted bytes → parsed module → the analysis those proofs are about.That is the toolchain's recurring fault class, applied to scry: a guarantee that is not enforced on the path that executes. A sound analyzer that panics, hangs, or mis-parses a malformed/adversarial module has not violated its soundness theorem — it has bypassed it. For a DO-333-positioned tool, "the analyzer crashed on the input" and "the analyzer silently analyzed something other than the shipped module" are both qualification-relevant.
Suggested scope
cargo-fuzztarget over the module parser / analysis entry point; corpus seeded from the existing test wasm + the toolchain's bench modules. Kill-criterion: no panic, no unbounded run, on any input.fuzz.ymlmatching the pattern already used by rivet/loom/meld/sigil (smoke on PR, longer nightly).Item 2 is arguably the higher-value half: it closes the model↔implementation gap that a proof alone leaves open.
Not a soundness accusation
No mis-analysis is being reported here — this is a missing guard, found by surveying test surfaces across repos, not by observing a failure. Filing so the gap is explicit rather than implicit.
🤖 Filed via Claude Code from a cross-repo test-surface survey.