Testing, Fuzzing and Formal Methods
Introduction
This branch turns protocol claims into executable properties and applies complementary methods to find counterexamples. Testing begins at Statecraft v0 and grows with every module.
Why It Matters
Example tests miss sequences and boundary values; fuzzers can exercise meaningless domains; invariants can be vacuous; formal models can faithfully prove the wrong specification. Evidence is strongest when methods disagree productively.
Mental Model
Create a ladder: specification → examples → fuzz domains → stateful handlers/ghost state → differential model → symbolic/SMT checks → mutation and failure injection. At every rung, record assumptions and coverage limits.
Questions This Branch Answers
- Which property expresses the protocol claim without becoming vacuous?
- Which state/actions can the harness actually reach?
- What new evidence does each testing technique contribute?
Scope
Forge unit/integration/fork tests, fuzzing, stateful invariants, economic properties, differential/model-based tests, symbolic/SMT work, mutation, gas/coverage, and failure injection.
Out of Scope
Claims of complete verification, paid-only platforms, checkbox coverage goals, mainnet attack execution, and formalizing an entire production protocol in the skeleton.
Dependencies
explicit state machines, reorg/finality models, and each project's written specification.
Candidate Note Roadmap
properties-examples-and-invariants— Separate expected examples from universal state properties.forge-unit-integration-and-fork-tests— Structure deterministic local and pinned-fork evidence.fuzzing-input-domains-and-assumptions— Generate meaningful values without hiding failure space.stateful-fuzzing-handlers-and-ghosts— Explore call sequences with auditable harness state.economic-invariant-design— Express conservation, solvency, shares, debt, and bounded extraction.differential-and-model-based-testing— Compare implementations against an independent executable model.symbolic-execution-smt-and-halmos— Search paths and prove scoped conditions with explicit bounds.mutation-gas-coverage-and-failure-injection— Test whether the suite notices broken logic and dependencies.
Future Project
A permanent Statecraft verification suite that grows from deterministic unit tests to stateful economic invariants, model comparison, mutations, symbolic checks, and injected dependency failures.
Initial Invariants
Assets reconcile with liabilities; balances and shares conserve declared quantities; signatures execute once; timelocks delay; liquidations remain bounded; cross-domain actions are idempotent; the harness reaches both success and failure states.
Initial Threat Model
Vacuous assertions, over-constrained inputs, unreachable actions, stale ghost variables, shared bugs between model and implementation, nondeterministic forks, false coverage confidence, and ignored external failures.
Primary Sources
Foundry, Solidity SMTChecker, Echidna, Slither, Halmos, and property-testing references curated in SOURCES.md.
Connects to: exploit labs, Statecraft, and every implementation branch.