Get started

Formal verification

Machine-checked
from state to proof.

The path from a state change to an accepted GKR proof is modeled and machine-checked in Isabelle/HOL, and a refinement theorem connects the shipped Rust verifier to that model under stated conditions.

Fully provedEvery theorem in the chain is machine-checked in Isabelle/HOL, none is admitted without proof, and all 20 proof files are rechecked on every change.
Every operationRecord present, absent and updated each compile to a circuit that accepts exactly the valid cases, proved in both directions.
One boundA single proved limit on how often a false proof can pass, from the state change to the verifier's answer, in the exact field the verifier uses.
Tied to the codeA refinement theorem connects the shipped Rust verifier to the model under stated conditions, with contracts across four areas of the code.

Trust chain

From a state change
to a verified proof.

Each link is a theorem the proof checker accepts. Together they bound the chance that the modeled verifier accepts a proof for an invalid state change.

  1. 01

    State semantics

    A formal meaning for membership, non-membership and single-leaf updates over empty, occupied and deleted leaves.

  2. 02

    Circuit compiler

    The compiled circuit accepts exactly the valid state operations, in both directions (Theorem A).

  3. 03

    GKR soundness

    A false claimed output survives the sumcheck and wiring reduction only within a proved probability bound (Theorem B).

  4. 04

    Composition

    The two results compose into one bound on the path from a state operation to its proof (Theorem C).

  5. 05

    Exact field

    The bound is carried to the degree-four extension field the verifier actually draws its challenges from.

A fourth theorem family covers batching: independent-job batch results agree with their single-job counterparts, preserving every acceptance and every rejection (Theorem D).

Formal verification paper · arXiv:2610.05335 (opens in a new tab)Theorems and sessions in the docs

Refinement

Tied to the Rust code,
under stated conditions.

A model matters only if the shipped code follows it. StateSync-GKR connects the two in two ways and states how far each connection reaches.

Verifier acceptance refinement

A theorem proves that whenever the shipped Rust verifier accepts, its acceptance trace falls inside the reduction-chain event of the verified GKR model, given a stated correspondence between the Rust trace values and the model. The formal verification documentation gives the exact statement and its premises.

Compiler

State semantics in code

Sparse-Merkle semantics, the compiler, the witness layout and selected primitives carry bounded contracts, backed by differential tests against the compiler theories.

Protocol

The reduction itself

Sumcheck, multilinear extensions, wiring and layer reduction. Round counting, rejection paths, transcript order and the final claim are translated as ordinary code.

Composed verification

The public entry points

Configuration, the composed verification path and the public facade, including an exact equality contract on the public-input binding.

Opaque primitives

Explicit seams

Field arithmetic, hashing and foreign constants enter as named assumptions, so the trusted surface is explicit.

Contracts are written in Creusot and checked through Why3 with automated solvers.

Scope

What the verification covers.

  • Sparse-Merkle semantics, the circuit compiler and GKR assembly are modeled and composed in Isabelle/HOL.
  • The soundness bound is proved over the exact extension field the verifier draws its challenges from.
  • The Rust code is tied to the model through contracts in four scopes, an acceptance refinement theorem, differential tests and adversarial vectors.
  • Every registered proof session is rebuilt from clean on each push to the maintained branch and weekly.

Each result is stated with its assumptions in the formal verification paper and the documentation, so an integrator can see exactly what an accepted proof rests on.

Results and assumptions in the docsIntegration boundaries

Research

Two papers, two kinds of evidence.

One paper machine-checks the argument. The other measures the engine. Together they say what the engine does, how well it does it, and under which conditions.

How to cite StateSync-GKR
Formal verification

StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification

A machine-checked Isabelle/HOL argument that the engine's circuits accept exactly the valid state operations, in both directions, and that a false claim passes the modeled verifier only within a proved probability bound, carried to the exact extension field the verifier uses.

Formal verification paper · arXiv:2610.05335 (opens in a new tab)
Design and evaluation

StateSync-GKR: Design and Evaluation of a Reusable Sparse GKR Engine

Connects the nine design mechanisms to controlled measurements of memory, preparation, verification, parallel proving and serving under load.

Design and evaluation paperarXiv link to follow
Independent review

Bernhard Müller (opens in a new tab) wrote the independent review of the verifier's challenge-generation assumptions (opens in a new tab), which is part of the source repository.

Security researcher. Creator of Mythril, the security analysis tool for Ethereum smart contracts, an author of the OWASP Mobile Application Security Testing Guide, and a 2009 Pwnie Award winner for Best Research.