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
Rootstock Flyover Quote Lifecycle
Formally verified peg-out quote conservation for Rootstock Flyover refunds.
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.
1delta Caller-Address Integrity
Formally verified caller-address integrity for scoped OneDeltaComposerEthereum transfer and callback fund-pull paths.
Usual DaoCollateral Conservation
Formally verified direct swap and redeem accounting for Usual USD0 DaoCollateral.
Piku Redemption Fund Conservation
Formally verified fund-conservation accounting for Piku queued redemptions.
Lagoon Guardrails PPS Compliance
Formally verified annualized PPS guardrail compliance for Lagoon v0.6.0 GuardrailsLib.
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.
Agglayer Bridge Claim Nullifier Guarantee
Formally verified claim membership and replay protection for AgglayerBridge.
Alchemix V3 Earmark Conservation
Formally verified earmark conservation invariant for Alchemix V3's lazy-accrual debt accounting system.
