AI-driven formal verification · a second tool alongside Certora
Machine-checked.
Never proofs of safety.
An AI pipeline that reads a Solana protocol's real source, proposes safety invariants, and discharges them on the open-source Certora Prover running locally on the compiled crate. Every result closes on a recorded command. Every build is re-checked by agents that did not write it — and the record of what's blocked is published next to what passed.
The number that isn't self-referential
Recall against a known-correct oracle
Auto-rate can be gamed; recall against an oracle cannot. A standing corpus pairs historical findings, an injected checked_div→checked_mul mutation, and regression cases with the answer known in advance. One command runs them all on the real prover.
How a run works
Four stages, one fail-closed router
The routine ~90% clears automatically; anything ambiguous — an unsigned assumption, an un-replayed counterexample, a timeout — escalates to a human. The tool never quietly upgrades a "maybe" into a "proved."
Read the source
Model families read the real Rust and propose candidate safety invariants — solvency, share-accounting conservation, rounding bounds, health monotonicity.
Adjudicate
An I80F48 simulator, anchored line-by-line to the source, tries to break each claim across millions of adversarial trials. Survivors only.
Prove
Surviving invariants compile into CVLR rules and run on the open-source Certora Prover, locally, against the actual compiled crate.
Route 90 / 10
A deterministic, fail-closed router auto-clears the routine and escalates the rest — with a counterexample that must replay on the real program before it counts as a finding.
Acceptance discipline
Twelve gates. Each closes on a command, never an argument.
The honesty is the product: a gate is either green on a recorded command, or it says blocked with the measured reason. Reporting the blocked one is the posture an FV evaluator trusts.
+ G13 — obligation → rule generator (standing product). A deterministic enumerator reads the guard-parity table and mechanically emits a prover rule per unguarded obligation — it reproduced the flagship finding with no human pointing at it, and then surfaced a genuinely new one on a second property.
Why more than one model
An adversarial gauntlet, judged by execution
Independent families take turns attacking the surviving catalog; the judge rules with the simulator, never by vote. A defect that one family missed, another has found — and the record shows it happening.
The last build round survived four successive adversarial verification passes — each one caught a regression the previous fix introduced, and each was closed with a pinned test. The pipeline is built to distrust its own results.
Flow sketch · how an engagement runs
Bring your program. Get a private report.
A concierge submission: the code owner opens a session, the crate is onboarded, the AI family runs the pipeline end-to-end, and the findings come back to the owner alone — never public first.
note Onboarding an arbitrary crate to build under the prover is the one step still done by an engineer today — it is the honest bottleneck, and automating it for a supported class of programs (standard Anchor + common dependencies) is exactly what the funded build turns self-serve, with CI re-verification on every pull request.
What we will not claim
The guardrails are part of the offer
"Proofs of safety"
Machine-checked properties under a signed, human-reviewed assumption ledger — not a blanket safety certificate the math can't support.
A Certora replacement
A complementary second tool for the STRIDE program, priced below the per-engagement manual anchor. The seat for a second FV vendor is open.
Public findings first
Every finding goes to the protocol team privately, under embargo, before any foundation or public mention. No exceptions.