Our Research
We are making formal verification practical and accessible to smart contract developers. Here's what we've published so far.
Publications
Case Studies
Lido V3 Vault Solvency Guarantee
A formally verified property of a production smart contract.
Safe Owner List Invariants
Formally verified linked list invariants of the Safe smart account.
Nexus Mutual Book Value Invariant
A formally verified price band property of the RAMM.
StreamRecoveryClaim Accounting Invariants
Formally verified claim accounting for the Sonic Earn Recovery System.
Reserve DTF Auction Price Band Invariant
Formally verified per-pair price band invariant for the auction pricing path in Reserve DTF Protocol.
ERC-7984 Confidential Token Invariants
Formally verified accounting properties of the Confidential Token Standard.
Wildcat Borrow Liquidity Invariant
Formally verified liquidity preservation for successful positive borrows in Wildcat V2.
Midas Growth-Aware Feed Safety Guarantees
Formally verified safety properties of the safe submission path in Midas's growth-aware price feed.
Cork Protocol Pool Solvency
Formally verified solvency invariant for the unwindExerciseOther function in Cork Phoenix.
TermMax Single-Segment Buy-XT Reserve Integrity
Formally verified reserve-update integrity of the single-segment debtToken-to-XT swap path.
Alchemix V3 Earmark Conservation
Formally verified earmark conservation invariant for Alchemix V3's lazy-accrual debt accounting system.
