Our Research
We are making formal verification practical and accessible to smart contract developers. Here's what we've published so far.
Case Studies
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
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
Explainers
When to Verify Bytecode Instead of Solidity
Why formal verification should usually model Solidity directly, and why the EIP-8282 builder predeploys were the exception.
What is a formal proof?
A short explanation for non-specialists.