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.
ForgeYields Gateway Solvency
Formally verified active-mode solvency accounting for ForgeYields TokenGateway.
Balancer ReClamm Swap Rounding Invariant
Formally verified product nondecrease for successful ReClamm swap quotes.
Alchemix V3 Earmark Conservation
Formally verified earmark conservation invariant for Alchemix V3's lazy-accrual debt accounting system.
