Certora¶
Status¶
Evidence required. No Certora specs, rule files, harnesses, or proof logs were found in the current local snapshot.
Candidate Specs¶
- Governor operation lifecycle cannot execute before queue and delay.
- Registered target kind must match policy assertions.
- Deposit intent consumption is one-way.
- Claim caps and executor scopes are enforced.
- Receipt source ids prevent double accounting.
- Settlement ordering preserves principal-first behavior.
Production Evidence To Archive¶
Spec files, harnesses, exact contract versions, solver/tool version, command line, proof result, assumptions, rule exclusions, and unresolved warnings.
Review Rule¶
Every proved rule must state its assumptions. If a role, oracle input, or external interface is modeled as honest, the limitation belongs in the evidence archive and threat model. A proof of a narrow property must not be summarized as proof of the whole protocol.
Evidence Model¶
| Field | Requirement |
|---|---|
| Purpose | rule-based formal verification of protocol invariants. |
| Expected location | Certora specs and prover reports. |
| 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 | specified rules over compiled bytecode/model abstractions. |
| What it does not prove | requirements not encoded as rules or trusted external assumptions. |
| 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 Certora 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.