SMTChecker¶
Status¶
Evidence required. No Solidity SMTChecker reports were found in the inspected snapshot.
Recommended Targets¶
- Arithmetic in reserve, receipt, smoothing, and settlement helper libraries.
- State transition assertions around settlement phases.
- Bounds on claim caps, exposure caps, and reserve locks.
- Impossible states for initialized seats and vault metadata.
Production Evidence To Archive¶
Solc version, SMTChecker settings, checked contracts, warnings, assertions, command output, and justification for every unresolved warning.
Integration Guidance¶
Start with small helper libraries and isolated assertions before attempting the full controller. Use SMTChecker output to support specific arithmetic or state assumptions, not as a broad protocol proof. Any warning that is suppressed or accepted must include an explanation and an owner.
Evidence Model¶
| Field | Requirement |
|---|---|
| Purpose | compiler-assisted bounded proof for assertions and arithmetic paths. |
| Expected location | Solidity compiler settings and emitted 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 | bounded properties the compiler can reason about. |
| What it does not prove | whole-protocol liveness or external system behavior. |
| 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 SMTChecker 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.