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.
Morpho Midnight Liquidation and Accounting Proofs
Machine-checked RCF recovery and bad-debt lender-credit accounting for Morpho Midnight, with pinned proof files and explicit Verity boundaries.
IPOR PlasmaVault Redeem Splitting
A formal-verification case study proving virtualized PPS safety for the public redeem arithmetic slice.
Term Finance TermAuction Clearing Assignment
Verified under documented assumptions: TermAuction assignment balances purchase-token principal at the clearing rate.
Zodiac Roles v3 Decoder Faithfulness
Formally verified calldata decoder faithfulness and bounds safety for the Roles v3 ABI walker.
Morpho Blue Health and Liquidation Invariants
Formally verified health preservation and a sharp full-liquidation guarantee for Morpho Blue, with explicit generated-body trust boundaries.
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.
Polaris Bonding Curve Reserve-Ratio Invariant
A Verity benchmark case for Polaris Finance bonding-curve checkpoint accounting.
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.
