Priority
Medium — should be addressed soon
User story / Problem statement
Before the external audit, the money-critical parts should have been checked by something other than
the tests that were written alongside them. This issue collects that work. It is deliberately open:
the tools, the depth and the order are to be decided as the contracts settle, and scoping it now
would fix choices that should stay open.
Candidates
- Kani over the conversion arithmetic. The rounding direction and the round-trip property are
small, pure, and provable without a host.
- Certora Sunbeam over the oracle guardrails and the vault's authority checks. Panics-family
rules are cheap and catch the most. Requires a fork of cvlr-soroban carrying a three-line fix,
since Cargo drops the member's default-features = false when the workspace entry omits it.
- TLA+ over the epoch state machine and the claim ordering. Checks interleavings the tests do
not reach, at small bounds, with a negative control per guard.
- Model-assisted review, with the contract and the design document read against each other.
- Static analysis and dependency audit in CI.
Notes
No acceptance criteria on purpose. Each candidate becomes its own issue when it is picked up, with
its own criteria and its own time-box. What belongs here is the record of what was considered, what
was chosen, what it found, and what was dropped and why.
A tool that finds nothing is worth recording as such. A negative control that turns green is a
failure, not a pass.
Refs: ARCHITECTURE §3 (Verification pre-audit), §6
Priority
Medium — should be addressed soon
User story / Problem statement
Before the external audit, the money-critical parts should have been checked by something other than
the tests that were written alongside them. This issue collects that work. It is deliberately open:
the tools, the depth and the order are to be decided as the contracts settle, and scoping it now
would fix choices that should stay open.
Candidates
small, pure, and provable without a host.
rules are cheap and catch the most. Requires a fork of
cvlr-sorobancarrying a three-line fix,since Cargo drops the member's
default-features = falsewhen the workspace entry omits it.not reach, at small bounds, with a negative control per guard.
Notes
No acceptance criteria on purpose. Each candidate becomes its own issue when it is picked up, with
its own criteria and its own time-box. What belongs here is the record of what was considered, what
was chosen, what it found, and what was dropped and why.
A tool that finds nothing is worth recording as such. A negative control that turns green is a
failure, not a pass.
Refs: ARCHITECTURE §3 (Verification pre-audit), §6