veritylabs

Our Research

We are making formal verification practical and accessible to smart contract developers. Here's what we've published so far.

Publications

Ethereum Verification Benchmark

Evaluating AI deductive reasoning for Smart Contracts.

Publication

Verity Verified Compiler

A Formally Verified Smart Contract Compiler in Lean 4.

Publication

Case Studies

Lido V3 Vault Solvency Guarantee

A formally verified property of a production smart contract.

for

Safe Owner List Invariants

Formally verified linked list invariants of the Safe smart account.

for

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.

for

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.

for

1inch XYCSwap Curve Safety

Formally verified fee-adjusted constant-product curve safety for 1inch Aqua XYCSwap.

for

Balancer ReClamm Swap Rounding Invariant

Formally verified product nondecrease for successful ReClamm swap quotes.

for

StarkGate Bridge Escrow Lower Bound

Formally verified escrow accounting for the StarkGate L1 token bridge deposit, withdrawal, and reclaim paths.

for

Pendle PY Supply Pairing

Formally verified PT and YT supply-pairing accounting for Pendle V2 mintPY and successful pre-expiry redeemPY paths.

for

Nexus Mutual Book Value Invariant

A formally verified price band property of the RAMM.

for

Aragon OSx Execute Authorization

Formally verified authorization admission, ROOT-gated permission mutation, and wildcard restrictions for a pinned Aragon OSx DAO slice.

for

Superfluid CFA Realtime-Balance Conservation

Formally verified conservation of CFA flow accounting, including a one-level callback.

for

LI.FI Swap Route Atomicity

Formally verified source-chain no-partial-success behavior for the original LI.FI GenericSwapFacet and SwapperV2 swap path.

for

Rootstock Flyover Quote Lifecycle

Formally verified peg-out quote conservation for Rootstock Flyover refunds.

for

KyberSwap Partial-Fill Price Floor

Formally verified helper-level partial-fill price-floor guard for MetaAggregationRouterV2.

for

Enzyme Onyx Dynamic Fee Accounting

Formally verified management-first fee ordering and exact owed-value accounting for Enzyme Onyx FeeHandler.

for

Alchemix V3 Earmark Conservation

Formally verified earmark conservation invariant for Alchemix V3's lazy-accrual debt accounting system.

for

Reserve DTF Auction Price Band Invariant

Formally verified per-pair price band invariant for the auction pricing path in Reserve DTF Protocol.

for

Zodiac Roles v3 Decoder Faithfulness

Formally verified calldata decoder faithfulness and bounds safety for the Roles v3 ABI walker.

for

Agglayer Bridge Claim Nullifier Guarantee

Formally verified claim membership and replay protection for AgglayerBridge.

for

ERC-7984 Confidential Token Invariants

Formally verified accounting properties of the Confidential Token Standard.

for

Wildcat Borrow Liquidity Invariant

Formally verified liquidity preservation for successful positive borrows in Wildcat V2.

for

Cork Protocol Pool Solvency

Formally verified solvency invariant for the unwindExerciseOther function in Cork Phoenix.

for

Term Finance TermAuction Clearing Assignment

Verified under documented assumptions: TermAuction assignment balances purchase-token principal at the clearing rate.

for

TermMax Single-Segment Buy-XT Reserve Integrity

Formally verified reserve-update integrity of the single-segment debtToken-to-XT swap path.

for

Midas Growth-Aware Feed Safety Guarantees

Formally verified safety properties of the safe submission path in Midas's growth-aware price feed.

for

IPOR PlasmaVault Redeem Splitting

A formal-verification case study proving virtualized PPS safety for the public redeem arithmetic slice.

for

Usual DaoCollateral Conservation

Formally verified direct swap and redeem accounting for Usual USD0 DaoCollateral.

for

Velora BridgeStaking Allocation Safety

In the Lean accounting model, under stated token and external-call hypotheses, allocated Velora VLR and WETH never exceed their modeled BridgeStaking balances.

for

StreamRecoveryClaim Accounting Invariants

Formally verified claim accounting for the Sonic Earn Recovery System.

for

YO Protocol Async Redemption Escrow Accounting

Formally verified pending-share and pending-asset accounting across YO redemption request, settlement, cancellation, and replay paths.

for

Lagoon Guardrails PPS Compliance

Formally verified annualized PPS guardrail compliance for Lagoon v0.6.0 GuardrailsLib.

for

T3tris HWM Performance Fee

Formally verified no-double-charge behavior for the T3tris high-water-mark performance-fee arithmetic slice.

for

1delta Caller-Address Integrity

Formally verified caller-address integrity for scoped OneDeltaComposerEthereum transfer and callback fund-pull paths.

for

Pareto Redemption Backing Guard

Checked the modeled depositFunds post-state under Pareto USP's source reserve require.

for

Polaris Bonding Curve Reserve-Ratio Invariant

A Verity benchmark case for Polaris Finance bonding-curve checkpoint accounting.

for

Piku Redemption Fund Conservation

Formally verified fund-conservation accounting for Piku queued redemptions.

for

ForgeYields Gateway Solvency

Formally verified active-mode solvency accounting for ForgeYields TokenGateway.

for

Hypernova Settled Payout Safety

A successful-path proof of settled-profit accounting, one-shot withdrawal closure, nonce consumption, and USDC payout bounds for pinned Hypernova contracts.

for