Problem
Property tests explore a wide input space but only along dimensions someone
thought to describe. For value-handling code, the highest-severity bugs tend to
live in state sequences nobody imagined — which is precisely what fuzzing and
formal methods are for.
What to do
cargo-fuzz targets over entrypoint arguments and, more importantly, over
sequences of calls. A single malformed call is rarely the bug; an
unexpected ordering usually is.- Run fuzzing on a schedule rather than per-commit, with a corpus committed so
coverage compounds over time.
- Evaluate formal verification for the settlement invariants specifically —
conservation of funds and the escrow state machine are small, high-value, and
well suited to it.
- Record the evaluation outcome either way, including a decision not to proceed
and why.
Acceptance criteria
Notes
Even a negative evaluation is worth writing down — "we considered formal
verification and chose fuzzing plus an audit because X" is a credible answer to
a question reviewers do ask.
Problem
Property tests explore a wide input space but only along dimensions someone
thought to describe. For value-handling code, the highest-severity bugs tend to
live in state sequences nobody imagined — which is precisely what fuzzing and
formal methods are for.
What to do
cargo-fuzztargets over entrypoint arguments and, more importantly, oversequences of calls. A single malformed call is rarely the bug; an
unexpected ordering usually is.
coverage compounds over time.
conservation of funds and the escrow state machine are small, high-value, and
well suited to it.
and why.
Acceptance criteria
Notes
Even a negative evaluation is worth writing down — "we considered formal
verification and chose fuzzing plus an audit because X" is a credible answer to
a question reviewers do ask.