Skip to content

Limitations

Current Gaps

Evidence required for Foundry, Echidna, Certora, SMTChecker, Slither, golden traces, Python/Solidity trace bridge, production deployment manifests, production role assignments, and per-runbook execution bundles.

Important Boundaries

  • The generated Solidity inventory is a documentation aid, not a compiler or proof.
  • The conformance harness is useful but not exhaustive formal verification.
  • The paper is a normative model reference, not deployed-code evidence.
  • Local source review cannot prove production addresses or role custody.
  • Passing mkdocs build --strict proves site integrity, not protocol safety.

Operational Effect

Before production, every claim of “tested,” “verified,” “deployed,” “role held by,” or “evidence archived” needs a concrete artifact path or transaction reference. Otherwise mark it “Evidence required.”

Evidence Model

Field Requirement
Purpose recording what current evidence does not prove.
Expected location gap register and accepted-risk notes.
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 known boundaries of assurance.
What it does not prove new safety guarantees.
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 limitations 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.