A Strata project

Formal verification for Solidity

Write specifications as NatSpec comments. StrataSolidity proves your contract meets them for all inputs and states, not just the cases you test.

Read the guide View on GitHub

token.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract Token {
    mapping(address => uint256) public balances;

    /// @custom:strata invariant totalSupply == sum(balances)
    uint256 public totalSupply;

    /// @custom:strata modifies balances[to], totalSupply
    /// @custom:strata ensures balances[to] == old(balances[to]) + amount
    /// @custom:strata ensures totalSupply == old(totalSupply) + amount
    function mint(address to, uint256 amount) external {
        totalSupply += amount;
        balances[to] += amount;
    }

    /// @custom:strata requires to != msg.sender
    /// @custom:strata requires balances[msg.sender] >= amount
    /// @custom:strata modifies balances[msg.sender], balances[to]
    /// @custom:strata ensures balances[msg.sender] == old(balances[msg.sender]) - amount
    /// @custom:strata ensures balances[to] == old(balances[to]) + amount
    function transfer(address to, uint256 amount) external {
        require(to != msg.sender, "self-transfer disallowed");
        require(balances[msg.sender] >= amount, "insufficient balance");
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }
}

strata-verify.sh token.sol

==== Verification Results ====
✅ Passed (11):
  invariant totalSupply == sum(balances) at line 4, col 1
  ensures balances[to] == old(balances[to]) + amount at line 11, col 9
  ensures totalSupply == old(totalSupply) + amount at line 12, col 9
  modifies frame (balances) at line 13, col 5
  invariant totalSupply == sum(balances) at line 13, col 5
  heap frame (only this contract is modified) at line 13, col 5
  ensures balances[msg.sender] == old(balances[msg.sender]) - amount at line 21, col 9
  ensures balances[to] == old(balances[to]) + amount at line 22, col 9
  modifies frame (balances) at line 23, col 5
  modifies frame (totalSupply) at line 23, col 5
  invariant totalSupply == sum(balances) at line 23, col 5

11 passed, 0 failed, 0 unknown out of 11 total

Without totalSupply += amount in mint

==== Verification Results ====
❓ Unknown (2):
  invariant totalSupply == sum(balances) at line 13, col 5
  ensures totalSupply == old(totalSupply) + amount at line 12, col 9

✅ Passed (8):
  invariant totalSupply == sum(balances) at line 4, col 1
  modifies frame (balances) at line 13, col 5
  ensures balances[to] == old(balances[to]) + amount at line 11, col 9
  ensures balances[msg.sender] == old(balances[msg.sender]) - amount at line 20, col 9
  ensures balances[to] == old(balances[to]) + amount at line 21, col 9
  modifies frame (balances) at line 22, col 5
  modifies frame (totalSupply) at line 22, col 5
  invariant totalSupply == sum(balances) at line 22, col 5

8 passed, 0 failed, 2 unknown out of 10 total

Real output from strataSolidity at commit 977b136 with z3. The invariant totalSupply == sum(balances) stops verifying the moment mint forgets to update the supply.

How it works

Solidity
solc AST
Lean translator
Laurel IR
Strata Core
VCG
z3

Specs live in your code

Specifications are @custom:strata NatSpec annotations: no imports, no stub functions, no separate spec language. solc is used only to produce the AST, so the compiler stays untouched.

One binary

The strataSolidity binary runs the whole pipeline. It invokes solc, parses the JSON AST into typed Lean structures, translates it, and verifies.

Built on Strata

Contracts are translated into Laurel, Strata’s intermediate verification language, and checked by Strata Core with an SMT solver.

Specification language

Annotation	Placement	Meaning
`requires <expr>`	Function	Precondition: must hold on entry
`ensures <expr>`	Function	Postcondition: must hold on exit. `old(expr)` refers to the pre-state
`invariant <expr>`	Contract or state variable	Assumed on entry and checked on exit of every public/external mutating function, assumed by view functions, and checked after the constructor
`modifies <vars>`	Function	Frame condition: only the listed state, or mapping keys, may change
`loop-invariant <expr>`	Function	Maintained across loop iterations
`forall v : T :: <expr>` `exists v : T :: <expr>`	Function	Quantifiers over all values of a type

Every annotation starts with @custom:strata. See the annotation reference.

Get started

Build from source. You need Lean 4 (via elan), solc, and z3 on your PATH. The Strata framework comes in as a git submodule.

Installation guide

git clone --recurse-submodules https://github.com/strata-org/Strata-Solidity.git
cd Strata-Solidity
lake build
Tools/Solidity/scripts/strata-verify.sh contract.sol

Add --sarif for SARIF 2.1.0 output, which GitHub code scanning can display on pull requests.

Where it stands

Works today

Simple and nested mappings, with old()
Contract invariants, including sum(mapping), checked across external calls that may re-enter the contract
Key-scoped modifies frame conditions
forall / exists with ==>
Loop invariants
Integer conversions, wrapping and signed division as the EVM performs them
Plain-text, JSON, and SARIF output, with counterexamples when z3 produces a model

Not yet

Struct fields accessed through mappings
old() in loop invariants
msg.sender in constructors
Reliable counterexamples: many violations still report ❓ unknown rather than a concrete model

Current limitations