Formal Verification Overview¶

This handbook does not claim full formal verification from the current local evidence. It documents confirmed local artifacts and the evidence still required before production claims.

Confirmed Local Evidence¶

Normative paper PDF exists at the refactor source path.
test_p10_conformance.js exists and encodes structural/source conformance checks.
build_all.sh, compile_one.js, package.json, and size JSON artifacts exist in the refactor package.
The current Solidity source removes the deposit false-freeze model and keeps governor finalFreeze as optional emergency machinery.

Referenced But Not Integrated Here¶

The handbook references Foundry, Echidna, Certora, SMTChecker, Slither, golden traces, and Python/Solidity trace bridging as desired assurance layers. Current local inspection did not find confirmed artifacts for those layers in this handbook repository or the inspected source snapshot.

What Each Layer Would Prove¶

Layer	Proves	Does not prove
Source conformance harness	Encoded structural expectations and selected scenario checks	Exhaustive correctness
Foundry/Echidna	Fuzzed invariants and transition properties	Human custody or deployed config correctness
Certora/SMTChecker	Stated formal properties under model assumptions	Properties not specified
Slither	Static-analysis findings for common bug classes	Economic correctness
Golden traces	Replayable expected scenarios	Unknown scenario coverage
Deployment manifests	Address and role evidence	Source correctness

Production Rule¶

Use Evidence Status as the source of truth. A missing artifact must remain “Evidence required.”

Evidence Model¶

Field	Requirement
Purpose	organizing all evidence layers and gaps.
Expected location	verification index, manifests, reports, and exceptions.
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	which evidence exists locally and which is missing.
What it does not prove	a blanket pass across all protocol 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 Verification overview 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.