Pre-audit verification

[hpmaxi]

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

[hpmaxi]

Forty adversarial questions were written against the code from the pricing, cancellation, oracle and role work, and are in the untracked working file docs/reviews/2026-09-10-security-questions.local.md. Four are rated Critical if real, and one is already stale because the oracle gained AccessControl after it was written.

The sharpest unanswered one: with the downward cap left unset, what bounds a single compromised attester crashing the price to min_answer and settling every open redemption there? min_answer, the cooldown and the guardian ripcord are the candidates, and none of them is a per-transaction bound.

Answering them belongs here rather than in a new issue. An answer of "no, because X" is worth recording next to the question.

[hpmaxi]

Answered: what bounds a compromised attester with the downward cap unset.

min_answer, and nothing else. Verified by test a_fall_is_bounded_only_by_min_answer: with max_down_bps = None a single attestation goes straight to the floor whatever the distance, and one stroop below is refused.

The attack sketch overstated it by using the test fixture's floor of 1 stroop. The reference deployment sets min_answer to 0.5e18, so a single report can halve the price and no more. That is severe but bounded, and it is the operator's choice.

The real defect was that nothing said so. min_answer reads like a sanity check and is in fact the downside risk parameter. Two corrections landed on this branch: the threat table said the cap bounds any single report, which is only true upward, and OracleConfig now records that the floor carries the bound.

What remains, and belongs to #75 rather than here: fulfill_epoch is permissionless and can consume an attestation in the same ledger, so there is no window for the guardian to react between a bad report and its use. A minimum age before an attestation can price an epoch would give one.