Formal verification

Tests check the inputs someone thought to try. Formal verification checks a claim for every input and every order of calls. You write what the contract guarantees in a spec file: facts that always hold about its storage, what each function does, and exactly when it reverts. A prover then checks each claim against the code.

Lithe is built to make this tractable. A contract's state only becomes visible to other code when a transition phase commits: a state-changing call to another contract runs after the phase, never halfway through it. So a claim about the contract can be checked one phase at a time, without modeling what the contracts it calls might do. In Solidity, every external call inside a function is a point where anything might have happened.

The compiler checks every spec: its types, what it may read, and the rules on this page. lithe prove proves a contract's specs for every input and every order of calls, and a test build checks every spec as the contract runs, so fuzzing and tests find a call that breaks one. Specs never change what is built: a contract compiles to the same bytecode with or without them.

Spec files

A contract's specs live next to it: vault.spec.lithe holds the specs of vault.lithe.

import "std/evm";
 
error Insufficient;
 
storage is record {
  total : wei;
  balances : map(address, wei);
}
 
external payable function deposit() is {
  storage.balances[Evm.sender()] := storage.balances[Evm.sender()] + Evm.value();
  storage.total := storage.total + Evm.value();
}
 
external nonreentrant function withdraw(const amount : wei)
  raises Insufficient
is {
  const have : wei := storage.balances[Evm.sender()];
  assert(have >= amount, Insufficient);
  storage.balances[Evm.sender()] := have - amount;
  storage.total := storage.total - amount;
  defer Evm.transfer(Evm.sender(), amount);
}

spec is {
  invariant ledger is storage.total = sum(storage.balances);
  invariant solvent is Evm.balance(Evm.self()) >= storage.total;
}
 
spec for withdraw is {
  const have : wei := old.storage.balances[Evm.sender()];
  raises Insufficient when have < amount;
  ensures new.storage.balances[Evm.sender()] = have - amount;
  ensures new.storage.total = old.storage.total - amount;
}

A spec file holds only spec blocks. For a file with one contract it writes them bare, as above. For a file with several, it wraps each contract's in spec for contract C is { ... }. lithe compile reads a spec file only to check specs as the contract runs, and lithe compile directory compiles no spec file as a contract.

Invariants

spec is { ... } holds the contract's invariants. An invariant is a bool that holds once deploy has run, and again each time a transition phase commits. Those are the only points where another contract can see or act on this one's state.

spec is {
  invariant ledger is storage.total = sum(storage.balances);
}

An invariant describes one state, so it reads storage as code does: storage.total, settings.feeBps, Module.domain.x.

Function specs

spec for f is { ... } describes one function: an entrypoint, a dispatched route such as setFee, a guard, or an internal function. The block sees f's parameters. A dispatched route's parameter is what its arm binds.

A function spec talks about two states: before the call and after it. Every read of something the call can change says which one it means:

old. and new. apply to the whole path after them, keys included. Parameters, Evm.sender(), Evm.value(), block and transaction context, immutables, and pure functions are the same in both states, and are read bare. A bare read of state is an error:

spec for withdraw is {
  ensures storage.total = 0wei;
}

say which state this reads: `old.` before the call, or `new.` after it

An old. value is read before the call, so no part of it can read new. state: new.storage.m[old.storage.k] is a value, but old.storage.m[new.storage.k] is an error.

Clauses

A reverted call has no after state, so raises and panics conditions read only old., directly or through a const.

When a function reverts

A spec block's raises and panics clauses are the complete list of the ways the function reverts. When the call reverts with E, one of E's conditions holds, and when it reverts at all, one of the listed conditions holds. A block with no raises or panics clause claims the function never reverts.

Some reverts are never listed, because no state before the call decides them: ABI decoding, ether sent to a function that is not payable, the reentrancy lock, a deferred call or continuation that fails, and running out of gas.

spec for f is partial { ... } drops completeness: its conditions still cause the reverts they name, but the function may revert in other ways too.

spec for transfer is partial {
  raises Insufficient when old.storage.balances[Evm.sender()] < amount;
}

Guards

A spec for a dispatch guard says when the guard reverts, and holds only raises and panics clauses. Every route through the guard inherits them, so an owner-only route's own spec does not repeat the owner check:

import "std/evm";
 
error NotOwner;
 
type OwnerAction is
  | SetFee external setFee of uint
  | Pause external pause
 
type Action is
  | Owner of OwnerAction
 
storage is record {
  owner : address;
  paused : bool;
  fee : uint;
}
 
function ownerMain(const action : OwnerAction)
  raises NotOwner
is {
  assert(Evm.sender() = storage.owner, NotOwner);
}
with case action of {
| SetFee(fee) -> { storage.fee := fee; }
| Pause -> { storage.paused := true; }
}
 
external function main(const action : Action)
  raises NotOwner
is
  case action of {
  | Owner(a) -> ownerMain(a)
  }

spec for ownerMain is {
  raises NotOwner when Evm.sender() <> old.storage.owner;
}
 
spec for setFee is {
  ensures new.storage.fee = fee;
}

With the guard's clause, spec for setFee says that setFee reverts only when the sender is not the owner, and otherwise sets the fee. A case added to OwnerAction inherits the guard's spec as it inherits the guard.

Modules

spec for module M is { ... } holds a module's specs: its invariants read the module's storage and that of the modules it requires, and spec for f names one of its functions. A module's specs are checked for each contract that uses the module, as its functions are.

import "std/evm";
import "std/interfaces/erc20";
import "std/token/erc20";
 
contract Token is {
  use ERC20 exposing IERC20;
 
  hook ERC20.beforeTransfer is skip;
  hook ERC20.afterTransfer is skip;
 
  deploy() is {
    ERC20.init("Token", "TKN");
  }
}

spec for module ERC20 is {
  spec for move is partial {
    raises ERC20InsufficientBalance when old.erc20.balances[from] < value;
    ensures new.erc20.totalSupply = old.erc20.totalSupply;
  }
}

A file a contract imports can have a spec file too, beside it, with spec for module M blocks for its modules; the spec tools read it for each module the contract uses. The standard library's do: ERC20's states that its balances add up to its supply and that the zero address holds nothing, and lists exactly when transfer, approve, and transferFrom revert; ERC721's that each owned token counts once in its owner's balance and that only a token that exists has an approval; Ownable's, Ownable2Step's, and AccessControl's that only the owner, or a role's admins, change who holds it, and exactly as asked; ERC1155's that an operator approval is set as asked, that a transfer moves the amount only for the owner or an operator it approved, when a batch transfer rejects its sender or receiver, and when a batch balance read rejects its lists. lithe prove proves them for each contract that uses the module, since the contract's own code can write the module's storage too. To prove a file of modules on its own, run lithe prove on it: lithe prove std/token/erc20.lithe proves the module as a contract that uses it, exposes all its external functions, and skips each hook it reaches.

Specs in the source file

A spec block can also sit in the source file, where a declaration can, or inside a module. The compiler then checks it as part of every build, and a wrong one fails the build. Keep specs in the spec file unless a module ships them itself.

Proving specs

lithe prove vault.lithe proves the specs of vault.lithe and its spec file against the EVM bytecode lithe build emits for it, the creation code and the runtime, with the Z3 solver: each invariant in each phase, and each claim of each function spec. A proof holds for the bytes that are deployed, with no trust in the compiler: where the optimizer is wrong, a claim fails. It takes lithe build's flags, such as --evm-version, and builds what lithe build would. Install Z3 first: brew install z3 on macOS, sudo apt install z3 on Debian and Ubuntu, or a release on your PATH. Without it, lithe prove says so and exits 2.

lithe prove vault.lithe

runtime code: 231 bytes, keccak256 0x0a069ffbf78b52094ac68047ed56d9512e77a96ded629d435aecf95bc5c1bc5f

storage types: each word the layout places holds its fields' types
  proved      the initial state
  proved      deposit
  proved      withdraw
  proved      balanceOf (unchanged)
  proved      calldata that names no function (unchanged)

invariant ledger: storage.total = sum(storage.balances)
  proved      the initial state
  proved      deposit
  proved      withdraw
  proved      balanceOf (unchanged)
  proved      calldata that names no function (unchanged)

spec for withdraw
  proved      ensures new.storage.balances[Evm.sender()] = have - amount
  proved      ensures new.storage.total = old.storage.total - amount
  proved      raises Insufficient when have < amount
  proved      raises Insufficient only when have < amount
  proved      reverts in no other case

24 proved, 0 failed, 0 unknown

The report names the runtime by its size and hash, so a proof can be matched to the code on a chain. What a proof covers says how the prover runs the bytecode.

lithe prove also proves the specs of the source with the source prover, which takes a fraction of the time. The bytecode's verdict is the result; under a claim the bytecode does not prove, the report shows the source's verdict too: a counterexample in the source's terms, or a claim the source proves, which the bytecode breaks. lithe prove --source runs the source prover alone, as a quick first pass while writing specs.

lithe prove finds Z3 in LITHE_Z3, then on PATH, or where --solver says, and gives each question --timeout seconds of the solver's CPU time, 30 by default, so a busy machine takes longer but proves the same. It exits 0 when everything is proved, 1 when a claim fails, 2 when it finds no Z3, and 3 when something is unknown or not proved.

Invariants

A phase is deploy, or the empty storage of a new contract when there is no deploy, each entrypoint's body, each continuation, and each migration. The prover assumes every invariant holds before a phase and proves each still holds after it. The first phase starts from nothing, so together they cover every order of calls. A continuation starts from any state the invariants allow, because other calls may run between its call and it. The contracts a phase calls need no modeling, because their calls run after it commits. A phase that changes nothing an invariant reads is proved and marked (unchanged). The way a facet calls a hook back into the contract is no phase of its own: the hook runs inside the transition whose module code calls it, as it does when the module is not delegated.

A migration's state is its previous version's, so the prover assumes nothing before one.

Function specs

A function spec's claims are about one call, from the state before it to the state its first phase commits. An entrypoint's call, and a module's external's, starts where the invariants hold, so a spec can rely on them: withdraw reverts in no other case because the ledger rules out an underflow of the total. An internal function runs inside a phase, before the phase may have put its state right, so its call starts from any state. A route answers for its own block and for the blocks of the guards it runs through; a route with no block of its own answers for its guards'.

Counterexamples

When a claim can fail, the prover shows how: the calldata, the caller, what the claim reads, and, for a claim about reverts, what the call reverts with. Under it is the source's verdict, with its counterexample in the source's terms: the arguments by name.

invariant ledger: storage.total = sum(storage.balances)
  proved      the initial state
  FAILED      deposit
              calldata = 0xd0e30db0
              Evm.sender() = 8192
              Evm.value() = 1
              storage.total before = 21840
              sum(storage.balances) before = 21840
              storage.total after = 21840
              sum(storage.balances) after = 21841
              in the source: FAILED
                Evm.sender() = 5
                Evm.value() = 1
                storage.total before = 0
                sum(storage.balances) before = 0
                storage.total after = 0
                sum(storage.balances) after = 1

A claim that fails of the bytecode but is proved of the source reads in the source: proved, so the bytecode does not do what the source says: the compiler emitted code that breaks it. A claim the bytecode proves shows the source's verdict only when the source fails it, which the source prover's model explains: it assumes less, such as a balance that could pass 2²⁵⁶.

Loop invariants

A loop the prover cannot follow one iteration at a time leaves it knowing only that what the body writes has changed, and a claim that depends on it is not proved. A loop invariant says more. It is a bool that holds each time an iteration starts, and when the loop ends, written after the loop's bound:

const start : uint := storage.steps;
for i : uint in 0 .. n bound 100 invariant storage.steps = start + i do {
  storage.steps := storage.steps + 1;
}

The prover proves that the invariant holds as the loop starts, with its counter at the start of the range, and that each iteration keeps it. Then, after the loop, it knows the invariant holds with the counter at the end of the range: here, that the steps went up by n. The report lists each loop invariant's claims under loop invariants, and a proof that relies on one that is not proved is unknown. A loop may have several invariants, and they may use sum, count, and forall; a build drops them, so they never change the code. A checking build checks each as every iteration starts. Loops in the bytecode says how the prover finds each loop in the code.

A sum or count is a running total the solver knows only in part: that it is at least any one value of its map, and any two at different keys. That is enough for a ledger, and when a proof fails, the prover checks that the counterexample's totals can be real sums before it reports FAILED. Beside a forall it cannot check that, so it reports not proved.

The prover assumes no call comes from the zero address, which no one has the key to: Evm.sender() and Evm.txOrigin() are never zero.

The contract's ether counts every value its deferred calls send as gone when the phase commits, the least it can hold until the next phase. Write invariants about it as lower bounds, such as Evm.balance(Evm.self()) >= storage.total: ether can arrive without a call.

What a proof covers

The prover runs the bytecode, phase by phase:

So malformed calldata is covered too: a word that encodes no value of its type, calldata cut short, or junk past the end. The prover runs the code path by path, over 256-bit words. A branch it cannot decide splits the path in two, and a loop is proved by induction at its head, as loops in the bytecode says. A path that jumps to a target it does not fix is cut, and the claims it reaches are unknown.

The specs read the bytecode's state through the layout map the compiler emits: the slot of each storage path, a field's bytes in a shared slot, and how a map derives the slot of a key, as lithe storage lists them. The prover checks the map before it uses it: no two places share a bit of storage. A sum or count is a running total the prover updates at each store to a slot of the map; a store it cannot place off every map a spec adds up makes its claims unknown.

A call to other code, or a creation, is where a phase commits in the bytecode: the invariants must hold there, as at the end. Past it, the prover forgets what other code can change, storage, balances, and return data, and assumes only what every phase keeps, the invariants; a continuation is that code, from that state. A staticcall, or a call to a precompile that sends no ether, changes nothing, and answers anything. A function spec's new. state is the state at the call's first commit, or at its end.

A revert claim is about calldata that encodes the function's arguments, with no ether sent to a function that is not payable, and the reentrancy lock free, as the reverts the completeness rule never lists. raises E when c proves the call reverts when c holds; raises E only when c proves that revert data starting with E's selector comes only when c holds; panics when c proves it reverts with Panic(uint256). A record parameter's fields are arguments of their own, as the ABI lays them out. A bytes, string, list, or tuple argument of dynamic size is encoded when the decoder takes it, as Solidity's does: its offset and its length fit in 64 bits, its length word and every byte or element are inside calldata, wherever its offset puts them, and each word of a narrow type, such as an address, is a value of its type. A value nested in another, such as the strings of a list(string) or the bytes field of a record in a list, is encoded the same way, at the offset its list's or record's head gives, counted from where that list's elements or that record's heads start. A spec reads a list argument's .length, and the elements of a list of words. Well-formed calldata runs twice for a function with a bytes, string, or list argument: with the first such argument right after the heads, where the ABI puts it, and with it anywhere else. In the second, the argument's offset is a number the solver does not know, so each bound the decoder checks is a sum it must show does not wrap, which makes some questions far harder: a claim can be proved in the first run and unknown in the second, as reverts in no other case of a function that takes a list(list(uint16)) is, and what a one-element batch transfer does to ERC-1155 balances.

Storage in the bytecode is words, which can hold what no Lithe type can, such as an address with its high bytes set. The first section of the report proves that no phase writes such a word: each word the layout places holds its fields' types, and the bytes no field takes are zero. Every other proof stands on it, so when it is not proved, they are unknown.

Loops in the bytecode

A loop is proved by induction at its head, where each iteration starts. When lithe prove builds the code, the compiler also emits a certificate for each copy of each loop in it: where its head and its exit are, and where its counter and each local of its function are at the head, on the stack, in a word of memory, or in calldata. Of the bytecode, the prover then proves:

The paths that leave the loop go on from that state, so past the loop the prover knows its invariants, and all it left as it was. Which parts of the state the iterations change, the prover finds by running them: words on the stack, memory, and storage, by the map, record, or string a slot belongs to. It finds two kinds of facts itself, and proves them like the invariants: a word each iteration moves by the same amount is that many steps from its start, and a counter that starts at or below its limit stays there. A proof through a loop whose invariants are not proved is unknown.

Nothing in a certificate is trusted. The induction holds for any head and any places a certificate names: a wrong one gives invariants that do not hold where it says, so their claims fail, or a loop the prover cannot summarize, whose paths are cut. The build that makes the certificates is the one lithe build emits: the compiler builds the code it chose again, with each pass noting where it moves the loops' labels and words, and keeps the certificates only if the bytes are the same.

A loop the compiler emits on its own, such as one that copies a list, stores a string, or checks each element of an argument, has no certificate and no invariants. When a path goes around one twice without knowing how many turns it takes, the prover summarizes it in the same way, with only the facts it finds. A routine the compiler calls that such a loop runs in, as the decoder of each inner list of a list(list(uint16)), runs once for each shape of the state it is called in, from a state whose words and memory are values it knows nothing of, and each call takes what that run found with its own values in their place; a routine that reads or writes storage, calls out, or hashes runs at each call instead. A loop with a known count runs turn by turn. So does a loop of the source without invariants, such as one over a list literal, until a path has forked at its exit test twice, so a run of no iterations and one of a single iteration are exact; from its head after that, it is summarized with only the facts the prover finds.

What a proof trusts

A counterexample that rests on what the prover only approximates, such as a precompile's answer, an EXP of an unknown power, a store at a constant slot the layout does not name, which a hash could land on, or a state at a loop's head that no iteration may reach, is not proved.

An internal function's spec is proved of each body the build compiles once, which its calls jump to. The compiler certifies where the body starts and where its parameters are there; the prover runs it from there, in any state, as an internal function's call starts, to the jump back to its caller. A function the build inlines into a call is proved of each copy, the same way: the compiler marks where each copy starts and ends, and where its parameters are as it starts, and the prover runs it from there, in any state and with the stack its caller left unknown, to its end. The optimizer moves code across a copy's boundary, so the compiler keeps a mark only where every instruction that writes, logs, calls, branches, halts, or reads storage stays on its side; when a pass merges a copy with the code around it, such as a read of storage another copy just wrote, the spec is unknown, and the entrypoints that call it answer for it. Over the examples and the standard library, 452 of 539 inlined copies keep their marks. The rest are merged for good: a copy's overflow check joined with its caller's into one branch, its code moved into a helper other call sites share, or its end merged into a tail other code jumps to. A boundary there would put the caller's code inside the copy, or the copy's end past a return it cannot follow, so those specs stay unknown. A guard runs at the start of each route through it, inlined, and the compiler marks where the guard's statements end in each route's code: its own reverts in no other case is proved of the reverts before that mark, wherever the route adds reverts of its own past it.

The prover reports as unknown a delegatecall to code the build did not produce, such as a fallback that passes its call on.

A selfdestruct ends its frame and sends the contract's ether to the account it names, which runs no code; since Cancun the contract stays, and one created in the same transaction goes as if it had never been, so only its deploy brings it back. A function a spec calls is read in the state the spec reads, with a spec's exact arithmetic: its constants, its ifs, and its value.

Facets, hooks, and upgrades

A contract that marks a module delegated is proved as one system: its router and its facets, on the contract's storage. A delegatecall into code the build produced runs that code there, in the caller's context: a facet, at the address the CREATE2 factory gives its creation code, which the prover runs to check that it returns the facet; or the contract's own code, when a facet calls a hook back. A staticcall into a facet runs it in the facet's own account, where nothing can change.

A facet calls a hook back through an entrypoint of the contract that runs only while a flag in transient storage is set, as the facet sets it for the call. A section of the report proves that the flag is clear whenever other code can run, at every call out and every end, so that no one else can reach a hook; every other proof stands on it.

An upgradeable contract is proved as the implementation behind its proxy. Its deploy runs on the proxy's empty storage, as the proxy's constructor runs it, and a migration from any state. upgradeToAndCall hands the contract on with its delegatecall into the implementation it installs: there the phase commits, and the invariants must hold. Whatever that code does belongs to the version it is: a later version's migration and phases answer for it, and when it is this version, the call is one of its own phases. Past the handover a path may only clear the flag a migration checks, and end.

Deployed code

--code proves code from a chain, rather than the build's, against the source's specs and layout. It takes the runtime as hex, or a file of it, such as cast code prints:

lithe prove --code "$(cast code 0x5FbDB2315678afecb367f032d93F642f64180aa3)" vault.lithe

The report gives the code's hash, marked as given, and every phase runs the given code. The initial state is proved only when the source's creation code returns exactly that code. Otherwise its rows are unknown: the other rows prove that each phase of the given code keeps the invariants, which says nothing of a contract until they hold once.

The source prover

lithe prove --source proves the specs of the source as written: the program the compiler checked, before it emits code. It trusts the compiler to translate it, so its proof says nothing of the bytecode, but it is fast, and its counterexamples name the arguments. lithe prove runs it too, and shows its verdicts beside the bytecode's where they explain one. With --source the report has no runtime code and no storage types section, and the counts are the source's.

The source prover models storage words, maps, records, checked arithmetic, and forall exactly, and runs internal calls, branches, and loops of up to 16 iterations. It does not model everything: strings, bit operations, and lists of records or strings become values it knows only the type of, and a spec cannot use them. A list whose length the code fixes, such as a literal [a, b], is the exception: the prover knows each element. So is a list of words a function takes, or one a loop pushes to: the prover knows its length and its elements, and a loop over it runs turn by turn as far as it may be short, the first 16 elements. When a counterexample depends on one of those, the report says not proved, and names what it approximated. What it cannot check at all is unknown, with why: a deferred Evm.delegateCall, and a fallback that passes its call to other code. A loop that may run more than 16 times, or over a list whose length it does not know, needs loop invariants. It proves each continuation as a phase of its own, and each internal function's spec of the function's source, wherever the build would inline it.

Checking specs as the contract runs

lithe compile --check-specs vault.lithe builds the contract with its specs checked on every call, for tests and fuzzing. A call that breaks a spec reverts with SpecViolation(string), whose message names the spec:

A test run cannot check the rest of what a spec claims: that a reverting call reverts with the error its spec names, and that it reverts in no other case. lithe prove does.

sum and count of a storage map are kept as the contract runs: the build updates a running total, in storage of its own, at each write to the map. A clause with forall, or with a sum or count of anything but a storage map, cannot be computed; the build skips it with a warning. The build also skips a contract's spec for an external that a module provides, which runs the module's code: write it in the module's spec.

A checking build computes a spec's arithmetic over the integers, as the prover does: a comparison of sums, differences, products, or quotients is exact, however large or negative the values in it, up to 512 bits. A product past that stops the call with SpecViolation, since the build cannot compute it. A spec value used as something other than a number, such as a map key, is computed as its type, so arithmetic there that overflows still panics. It reads the spec file, runs every module in the contract, even a delegated one, and is bigger and slower than the plain build. Don't deploy it.

Spec-only forms

sum and count range over every key, which only a spec can: a contract cannot enumerate a map. Inside a spec block, old, new, sum, count, and forall are these forms. Outside one, they are ordinary names.

A spec cannot query another contract or read Evm.gasLeft.

lithe specs

lithe specs file.lithe checks the file's specs and its spec file's, and lists what each block claims:

lithe specs vault.lithe

spec is
  invariant ledger: storage.total = sum(storage.balances)
  invariant solvent: Evm.balance(Evm.self()) >= storage.total
spec for withdraw(amount : wei) (entrypoint)
  const have := old.storage.balances[Evm.sender()]
  raises Insufficient when have < amount
  ensures new.storage.balances[Evm.sender()] = have - amount
  ensures new.storage.total = old.storage.total - amount
  reverts in no other case

A guard's entry names the routes through it, and a route's entry names the guards whose clauses it inherits.