Our work

Verity: Smart Contracts You Can Prove Correct

Verity is an open-source language and compiler for Ethereum smart contracts. You write a contract, write down the rules it must follow, and prove that it follows them in every case, not just the ones you tested. LFG Labs builds Verity with a grant from the Ethereum Foundation.

Built by: LFG Labs
Grant from: Ethereum Foundation
License: MIT

Overview

What is Verity?

A smart contract does exactly what its code says, and it often controls real money. When the code has a mistake, nobody can step in and say that was not what the team meant.

Verity lets you catch those mistakes before a contract ships. The contract logic, the rules it must follow, and the proofs that it follows them all live together in one codebase. They are written in Lean 4, a programming language that can also check mathematical proofs.

Verity then compiles the contract to the bytecode Ethereum runs. The compiler comes with proofs of its own, so the meaning of the contract is preserved along the way.

Thomas MarchandVerity lead

Why Verity

Why Verity is useful

Tests and audits are valuable, but they can only show that bugs exist, never that none remain. A proof answers a different question: does this rule hold in every case?

Method	What it tells you	What it cannot tell you
Tests	The cases you wrote behave as expected.	What happens in the cases you did not write.
Audit	Experts looked for bugs and attack paths, and what they found.	Whether any bug remains.
Formal proof	A rule holds in every case, under stated assumptions.	Whether you wrote the right rule.

It covers the cases nobody imagined. A proof does not depend on someone thinking of the right scenario. If a strange input could break the rule, the proof does not go through.

Anyone can check it. You do not have to take our word for it, or trust the AI that helped write the proof. Lean checks the proof by machine, and anyone can run that check again.

It keeps working through upgrades. An audit describes the code on the day it was reviewed. A proof is checked again whenever the code changes, so a change that breaks a rule shows up right away.

It handles hard math. Solver-based tools struggle with non-linear arithmetic, which is why the solvency invariant of Lido V3 StakingVaults had stayed unproven. With Verity, we proved it.

Full proofs used to be too slow and expensive for most teams. AI is changing that: agents can now do much of the proving, and because Lean checks every step, their mistakes cannot slip through. We bet that agents will make full formal verification practical.

How it works

How Verity works

Take a simple token. There is one rule you would certainly want: a transfer moves tokens between accounts, and it never creates or destroys them.

Write the contract

You write the contract in Verity, in a language that reads much like other smart contract code. Here is the transfer function from a token example in the repository.

function transfer (toAddr : Address, amount : Uint256) : Unit := do
  let sender ← msgSender
  let senderBalance ← getMapping balancesSlot sender
  require (senderBalance >= amount) "Insufficient balance"

  if sender == toAddr then
    pure ()
  else
    let recipientBalance ← getMapping balancesSlot toAddr
    let newRecipientBalance ← requireSomeUint
      (safeAdd recipientBalance amount) "Recipient balance overflow"
    setMapping balancesSlot sender (sub senderBalance amount)
    setMapping balancesSlot toAddr newRecipientBalance

02
Write down the rule
In English, the rule is: when tokens move between two accounts, the sum of all balances stays the same. In Lean, that sentence becomes a precise statement about every sender, every recipient, every amount, and every starting state.
03
Prove it
A proof is a step-by-step argument that the code obeys the rule. A person or an AI agent writes it, and Lean checks every step. If one step is wrong, the build fails.
Read this proof
04
Compile and deploy
Verity compiles the contract to EVM bytecode, ready to deploy. The rule and the proof stay next to the code, so the next person to change the contract has to keep them true.

Verified compiler

Why the compiler is verified too

Ethereum does not run the code you proved. It runs bytecode, so a compiler bug could break a contract whose source was perfectly correct. Verification tools usually work on either the source or the bytecode, which leaves a gap between the rules you wrote and the code that runs.

Verity narrows that gap. It translates a contract in three stages, down to Yul, a low-level language for the EVM. Each stage has a proof that the translation keeps the contract's meaning. The final step from Yul to bytecode uses the standard Solidity compiler, pinned to a fixed version, and that step is trusted rather than proved.

The compiler proofs cover a core set of language features, and we keep widening it. The trust assumptions list exactly what is proved and what is trusted.

Limits

What a proof covers

A proof shows that the code follows the rules you wrote. It cannot show that you wrote the right rules. That is why most of the effort in a real engagement goes into deciding what to prove.

Every proof also rests on stated assumptions, such as how an external contract behaves. Writing them down is part of the value: you see exactly what your protocol depends on.

Using Verity

Two ways to use Verity

Verify an existing Solidity contract

Most protocols are already written in Solidity. For them, we model the contract in Verity, specify its invariants, and formally verify the model. Our Morpho Midnight proofs work this way. The proofs apply to the model, so the model has to match the original code closely. We are working toward Solidity parity so this flow keeps getting easier.

Write the contract in Verity

New contracts can be written directly in Verity and get formal verification from day one. The rules and proofs grow with the code, and the contract you deploy comes straight out of the verified compiler. We are already seeing developers build on top of Verity in this direction.

Contact our team

We take 4 protocols per quarter. Formal verification demands deep focus. We'd rather verify fewer contracts well than many poorly.

Learn more

What is a formal proof? A short introduction for non-specialists.

Read the research paper, accepted at ETHReS 2026, the Ethereum Research Symposium at ETHPrague.

Source on GitHub and documentation.

Verity Benchmark, which measures how well AI agents prove real contract properties.