Echidna¶
Status¶
Evidence required. No Echidna configuration, property contracts, corpus, or campaign output was found in the inspected snapshot.
High-Value Properties¶
- Consumed deposit intents cannot become usable again.
- Receipt and economic source ids cannot be double counted.
- Claims cannot exceed available rewards, caps, or settlement buckets.
- Settlement cannot pay reward remainder before protected principal rules are satisfied.
- Stop-loss, stale, or quarantined observations cannot enable ordinary claims.
Production Evidence To Archive¶
Config file, property contracts, corpus, seed, duration, tool version, command output, coverage summary, and minimized counterexamples for any finding.
Campaign Design¶
Separate fuzz campaigns by control plane: governance, deposit admission, receipt/source accounting, claims, settlement, and vault exits. This keeps failures interpretable and prevents a broad harness from hiding gaps in setup or coverage.
Evidence Model¶
| Field | Requirement |
|---|---|
| Purpose | property fuzzing for state-machine and accounting invariants. |
| Expected location | Echidna config and corpus directory. |
| Current local evidence status | Evidence required unless the named artifact is present in this repository or the Solidity source snapshot and has been inspected in the current run. |
| What it proves | classes of invariant violations under generated sequences. |
| What it does not prove | absence of bugs outside encoded properties. |
| How to regenerate | Run the documented tool from a clean environment, archive command, commit/source hash, config, stdout/stderr, and result files. |
| Production requirement | Results must be tied to the exact source manifest lock, compiler version, dependency lock, and deployment artifact under review. |
| Owner responsible | Protocol engineering owns source/test correctness; security review owns independent challenge; governance owns accepting residual risk. |
| Failure meaning | A failure blocks release, launch, upgrade, or operation until root cause is fixed or explicitly accepted with documented risk. |
Review Notes¶
Do not write “pass” for Echidna without current evidence. If evidence is missing, stale, or tied to a different source snapshot, write Evidence required and keep the gap visible in the release or operations checklist.