Formally Verifying WebAssembly Functions in Lean

Generative AI is making steady progress on mathematical research with Lean. Seeing that, I wondered—perhaps a little uncritically—whether Lean and WebAssembly could be combined. WebAssembly runs programs written in different languages on a common runtime, so maybe the same verification logic could apply to the same algorithm implemented in different languages.

WebAssembly, however, is a binary format for a virtual instruction set. Can a binary be formally verified?

In this article, I try formal verification by translating WAT into Lean function definitions, matching them against function bodies decoded from binaries, and checking a property.

What is formal verification?

Formal verification represents program behavior with a mathematical model and mechanically checks whether properties in a specification hold. Two common approaches are model checking, which explores state transitions, and deductive verification, which constructs a logical proof with a theorem prover. Here I try deductive verification, using Lean as the theorem prover.

As a large-scale example, Anthropic reports a collaboration with Theorem that verified 239 entry points across 123 OSS-Fuzz libraries. Claude proved that single-threaded, statically linked RISC-V binaries would not crash on inputs under 64 MB in a Linux model, and the Rocq kernel checked those proofs.

This article also focuses on compiled binaries rather than source code. I narrow the target to WebAssembly and use a small example to follow how a Lean execution model can be connected to an escrow business rule.

Here are a few resources on formal methods and Lean.

Verifying an escrow state transition

The example is payment handling for an online marketplace that connects buyers and sellers. After a buyer pays, the platform holds the money through a payment service until the transaction is complete. Once receipt of the goods is confirmed, the platform instructs the service to pay the seller. If the transaction falls through, it instructs the service to refund the buyer. Issuing both instructions for the same transaction would settle it twice, so only one may be issued.

The actual movement of money is handled by a higher-level payment process. This sample function updates state and returns a result code. I implemented the same state transition in C and Rust, with a safe version and a vulnerable version that leaves the transaction unsettled after paying the seller.

The state is represented by one byte, with state[0] holding the transaction phase. The three operations are funding, paying the seller, and refunding the buyer.

The safe version accepts a payout or refund only when the state is FUNDED, then moves to a terminal state. The vulnerable version leaves the state as FUNDED after paying the seller, so it also accepts a refund afterward.

Here is the state transition implemented in C and Rust.

#include <stdint.h>

enum {
    EMPTY = 0, FUNDED = 1, RELEASED = 2, REFUNDED = 3,
    FUND = 0, RELEASE = 1000, REFUND = 1000000
};

uint32_t escrow_step(uint8_t *state, uint32_t action) {
    uint32_t phase = state[0];

    if (phase == EMPTY && action == FUND) {
        state[0] = FUNDED;
        return 1;
    }
    if (phase == FUNDED && action == RELEASE) {
#ifndef VULNERABLE
        state[0] = RELEASED;
#endif
        return 2;
    }
    if (phase == FUNDED && action == REFUND) {
        state[0] = REFUNDED;
        return 3;
    }
    return 0;
}

#![no_std]

use core::panic::PanicInfo;

#[panic_handler]
fn panic(_: &PanicInfo) -> ! { loop {} }

#[no_mangle]
pub unsafe extern "C" fn escrow_step(
    state: *mut u8, action: u32,
) -> u32 {
    let phase = *state as u32;

    if phase == 0 && action == 0 {
        *state = 1;
        return 1;
    }
    if phase == 1 && action == 1000 {
        #[cfg(not(feature = "vulnerable"))]
        { *state = 2; }
        return 2;
    }
    if phase == 1 && action == 1000000 {
        *state = 3;
        return 3;
    }
    0
}

Build the C version with -DVULNERABLE or the Rust version with --cfg 'feature="vulnerable"' to omit the update that stores RELEASED after a payout. Both were compiled with -O2.

The operation codes passed to the Wasm function are 0 for funding, 1000 for paying the seller, and 1000000 for refunding the buyer.

The generated modules passed wasm-tools validate. Their sizes and SHA-256 hashes below identify the artifacts imported into Lean.

What we verify

Below, I use formal verification for the process from specifying a property to checking it, and proof for an individual property accepted by Lean.

An operation trace is any finite list of FUND, RELEASE, and REFUND. The safe version's specification says that executing a trace must not emit two or more settlement result codes, counting payouts to the seller and refunds to the buyer.

The vulnerable version has a concrete counterexample.

Result 2 means pay the seller; 3 means refund the buyer. If the higher-level process follows both instructions, the same transaction is paid out and refunded. This three-operation counterexample is short enough for a unit test. A test checks the traces it exercises. Lean goes further and proves that the safe version emits at most one settlement result for every finite trace made from the three defined operations.

Using Wasm as a common verification target

Functions implemented in different languages, such as C and Rust, can be compiled to Wasm and checked against the same Lean execution model and escrow specification. The model only covers functions that use supported instructions. This does not prove that the source programs are equivalent or that the compiler preserves the source semantics.

Following instruction execution requires tracking state such as the value stack and memory. It is natural for theorems to become hard to read when all that state appears directly in them. This is not unique to Wasm. CompCert relates execution states in C and assembly, while seL4 connects an abstract specification to a C implementation in stages. The theorem can state a business-level property while the execution model contains the state details.

To connect the property to the actual .wasm, I bring the function body into Lean through two paths. One path turns WAT into a Lean Func definition; the other decodes the function body directly from the binary bytes. The diagram shows how the decoded body is checked against the Func definition and then connected to the execution model and escrow specification.

Tools such as wasm-tools print convert .wasm to text-form WAT. My Rust transpiler, wat2lean, converts the function body into a Lean Func definition. The repository also includes a Lean library for Wasm syntax, binary decoding, and instruction execution.

habakan/wat2leanA WAT-to-Lean transpiler and WebAssembly execution and decoding librarygithub.com

Run cargo run from the root of the wat2lean repository.

wasm-tools print rust-safe.wasm > rust-safe.wat
cargo run -- rust-safe.wat 0 rustEscrowSafeCode > rust-safe.lean

This excerpt shows the condition for paying the seller in the safe version's WAT. local 2 is the current state, local 1 is the operation, and local 3 holds the next state and result code. It first checks whether the state is FUNDED (1), then whether the operation is RELEASE (1000). Only when both match does it set local 3 to 2.

local.get 2       ;; push local 2 (phase) onto the stack
i32.const 255     ;; push the mask value 255
i32.and           ;; restrict phase to the range 0–255
i32.const 1       ;; push FUNDED (= 1)
i32.ne            ;; push 1 if phase != 1
br_if 1           ;; if the condition is 1, branch to depth 1
block             ;; begin a block for the RELEASE condition
  local.get 1     ;; push local 1 (action) onto the stack
  i32.const 1000  ;; push RELEASE (= 1000)
  i32.ne          ;; push 1 if action != 1000
  br_if 0         ;; if the condition is 1, exit this block
  i32.const 2     ;; push the payout result and next-state value
  local.set 3     ;; store the value in local 3
  br 1            ;; branch to depth 1
end               ;; close the block

The next part writes local 3 back to the first byte of state and returns the same value.

local.get 0     ;; push the state pointer onto the stack
local.get 3     ;; push the next state
i32.store8      ;; write one byte to the first byte of state
end             ;; close the control block
local.get 3     ;; push the result as the return value

wat2lean converts WAT instructions into a Func made from constructors such as .localGet, .const, .bin, and .store8. The Lean codeBody decoder reads the function body from the original bytes. For each binary, we check that function 0 has type (2, 1) and that the decoded body matches the Func definition.

import WasmCode
open WasmCode WasmCode.Instr WasmShape

theorem rustEscrowSafeCodeMatchesBinary : isFunc (codeBody rustEscrowSafeBytes 0) rustEscrowSafeCode = true := by
  decide +kernel

theorem cEscrowSafeCodeMatchesBinary : isFunc (codeBody cEscrowSafeBytes 0) cEscrowSafeCode = true := by
  decide +kernel

theorem rustEscrowSafeTypeMatchesBinary : typeOf rustEscrowSafeBytes 0 = some (2, 1) := by
  decide +kernel

The same type and function-body theorems are included for the vulnerable C and Rust binaries. In WAT, we checked that the module has no imports and that function 0 is exported as escrow_step. However, Lean's codeBody assumes a module without imports when interpreting function indices, and the Lean proofs do not check the relationship between the import and export sections. The hashes identify the artifacts; they are not proof targets in Lean.

Defining Wasm instruction semantics

The rules that define how values and memory change when an instruction executes are called its semantics. The WebAssembly specification also defines execution states and transition rules. For example, i32.store8 writes one byte to linear memory, while br transfers control to a specified block. I define a Lean model for a subset of the rules in the execution section of WebAssembly 1.0 and use it to run instruction sequences.

The library represents the execution state with Store and Out. These are part of the execution model; the article's theorems do not need to expose all these fields directly.

namespace WasmCode

structure Store where
  mem : Nat -> UInt8
  size : Nat
  globals : List Nat

inductive Out where
  | normal (st ls : List Nat) (s : Store)
  | br (l : Nat) (st ls : List Nat) (s : Store)
  | ret (st ls : List Nat) (s : Store)
  | trap

end WasmCode

Store contains linear memory, its size, and global variables. Out.normal represents normal termination and contains the value stack, locals, and the updated Store. .trap represents a trap. execInstr is the function that executes an instruction; it also returns .trap when its fuel runs out. Fuel limits recursion in the Lean execution model. It is not a setting in the Wasm module.

More specifically, the type of execInstr is (fs : Nat -> Option Fn) -> Nat -> Instr -> List Nat -> List Nat -> Store -> Out. It takes a function table, fuel, an instruction, a value stack, locals, and a Store, and returns an execution result.

The library does not cover all of WebAssembly; it covers an explicit subset of instructions. Unsupported instructions either fail to decode or trap in the execution model. The theorems apply to this model and do not establish that it matches every rule in the full specification.

Connecting execution states to the specification

The previous section connected the Lean Func definition to the function body in the binary and introduced the instruction execution model. Here I convert one Wasm function call into the state and result code used by the escrow specification. Lean's wasmEscrowStep takes an escrow state and an operation, calls the function with execInstr, and extracts the updated state and return value when execution terminates normally.

The initial Store places the escrow state byte at memory address 2048 and sets all other memory to 0. The C version starts with 258 pages and a stack-pointer global [66576]; the Rust version starts with 16 pages and no globals.

However, wasmEscrowStep maps every result other than .normal to (phase, 0). So the one-step correspondence theorem only covers the state and result code extracted by this function. If a Wasm call traps for an input that should do nothing, this correspondence alone will not catch it. It does not prove that every call terminates normally. The settlement-count theorem also counts the result codes returned by wasmEscrowStep.

In the execution model, the head of the value-stack list is its top. The call therefore starts with [action, 2048]. The function-call implementation restores the argument order, passing the state pointer to Wasm local 0 and the action to local 1.

One step in the specification is defined like this:

def escrowSpecStep : EscrowPhase -> EscrowAction -> EscrowPhase × Nat
  | .empty, .fund => (.funded, 1)
  | .funded, .release => (.released, 2)
  | .funded, .refund => (.refunded, 3)
  | phase, _ => (phase, 0)

Return value 1 means funding was accepted, 2 means pay the seller, 3 means refund the buyer, and 0 means no operation was performed. The vulnerable version of the specification leaves the state as .funded after a payout, so the trace FUND, RELEASE, REFUND returns both 2 and 3.

We extend the correspondence for one step to any trace by induction. The diagram shows how the result extracted from Wasm is compared with the specification, leading to the property that the safe version emits at most one settlement result.

For each safe and vulnerable C and Rust implementation, we proved that the one-step result from wasmEscrowStep matches the specification's transition. By induction, the correspondence extends to traces of any length. For the safe versions, we get these theorems:

theorem cEscrowSafeTraceEmitsAtMostOneSettlementResult
    (actions : List EscrowAction) (phase : EscrowPhase) :
    settlementCount (cEscrowSafeTrace actions phase).1 <= 1 := by
  rw [cEscrowSafeTraceMatchesSpec]
  exact escrowSpecTraceSettlesAtMostOnce actions phase

theorem rustEscrowSafeTraceEmitsAtMostOneSettlementResult
    (actions : List EscrowAction) (phase : EscrowPhase) :
    settlementCount (rustEscrowSafeTrace actions phase).1 <= 1 := by
  rw [rustEscrowSafeTraceMatchesSpec]
  exact escrowSpecTraceSettlesAtMostOnce actions phase

Here actions is any finite list of FUND, RELEASE, and REFUND. settlementCount counts results 2 and 3. The C and Rust functions emit at most one settlement instruction in total.

For the vulnerable versions, we checked a concrete counterexample using the same Lean execution model.

def attackTrace : List EscrowAction := [.fund, .release, .refund]

theorem cEscrowVulnerableTraceEmitsTwoSettlementResults :
    settlementCount (cEscrowVulnerableTrace attackTrace .empty).1 = 2 := by
  rw [cEscrowVulnerableTraceMatchesSpec]
  decide +kernel

theorem rustEscrowVulnerableTraceEmitsTwoSettlementResults :
    settlementCount (rustEscrowVulnerableTrace attackTrace .empty).1 = 2 := by
  rw [rustEscrowVulnerableTraceMatchesSpec]
  decide +kernel

Finally, #print axioms in EscrowKernel.lean reports that the safe theorems depend on Lean's standard axioms propext and Quot.sound. The concrete counterexamples for the vulnerable versions depend only on propext. There are no unproved sorry placeholders.

Summary

• I compiled safe and vulnerable C and Rust implementations to Wasm and matched all four function bodies to the binary decoder's output.
• Using the Lean execution model and the results extracted by wasmEscrowStep, I formally verified that the safe versions do not emit duplicate settlement results for any finite trace.
• For the vulnerable versions, I showed that FUND, RELEASE, REFUND emits two settlement results.
• The model is limited to one transaction with a one-byte state, three operations, and instructions supported by the library. It does not cover actual money movement, amount calculations, or concurrency. Because results other than .normal are mapped to “no operation,” normal termination is not guaranteed. The proofs also do not establish conformance with the full Wasm specification, compiler correctness, or that the specification itself captures every business requirement.

This example shows how a compiled Wasm function can be connected to a readable state-transition specification and formally verified in Lean.