Formal verification

The StateSync-GKR compiler and GKR protocol are modeled and machine-checked in Isabelle/HOL. This page explains what those proofs state, how the Rust code is connected to them and which assumptions they rest on. The repository's FORMAL_VERIFICATION.md (opens in a new tab) holds the complete statement, and the formal verification paper (opens in a new tab) describes the development in full. Version 1.1.1 changed only distribution and package metadata; the Rust kernel and the formal sources keep their recorded contents.

The verification chain#

The development connects what a valid state transition means to the probability that a GKR verifier accepts a false claim:

1. Semantics: a formal semantics of sparse-Merkle membership, non-membership and update over empty, occupied and tombstone leaves.
2. Compiler: acceptance of the compiled layered circuit is equivalent to transition validity.
3. Protocol: a GKR assembly model bounds the probability that a false output claim survives the sumcheck and wiring reduction chain.
4. Composition: the compiler and protocol results compose, so the protocol bound transfers to semantically invalid transitions.

A further chain of sessions carries the protocol bound to the exact degree-four extension field that the implementation uses for challenges. A separate conditional theorem relates the shipped verifier's acceptance to the model event.

Registered sessions#

The development has six registered Isabelle sessions with twenty theories. They build on Isabelle2025-2 with no admitted proof. In session and theorem names, SMT abbreviates sparse Merkle tree, not satisfiability modulo theories.

The canonical theory sources are in formal/isabelle/ in the source repository.

What is proved#

The theorem families below use the public names from FORMAL_VERIFICATION.md and the paper.

Compiler semantic equivalence (Theorem A)#

Compiled-circuit acceptance agrees with sparse-Merkle operation semantics in both directions, for all three operations. The hash functions are abstract parameters, so the statement is a deterministic equivalence with no collision assumption. A separate lemma reduces leaf-hash collisions to collisions of the underlying sponge.

• Named theorems: theorem_A_soundness, theorem_A_completeness
• Canonical source: SMT_Semantics.thy, Compiler_Model.thy, Compiler_Correctness.thy

GKR assembly soundness (Theorem B)#

Against an arbitrary prover, a false claimed output survives the sumcheck and wiring reduction chain only with the proved probability bound. Per-round sumcheck soundness is imported from the Archive of Formal Proofs entry rather than re-proved.

• Named theorem: gkr_assembly_soundness
• Canonical source: Sumcheck_Instance.thy, Wiring_MLE.thy, Layer_Representative.thy, GKR_Assembly.thy

The same session proves that the derived wiring representation equals its table form under a stated repartition premise. The Rust derivation check and its fallback belong to the partial implementation connection described below.

Composition (Theorem C)#

The compiler and GKR results compose into one bound on the state-to-proof path for the named verification model. The witness is fixed before the challenge experiment.

• Named theorem: theorem_C_composition, with the composition results in Composition.thy
• Canonical source: Composition.thy, Compiler_Instance.thy, Composition_Instance.thy

Batching agreement (Theorem D)#

Independent-job batch results agree pointwise with their single-job counterparts, preserving acceptance and rejection. The theorem covers independent jobs. It says nothing about a single aggregate proof or scheduler liveness.

• Named theorems: theorem_D_batching_correctness, theorem_D_accept_preservation, theorem_D_reject_preservation
• Canonical source: GKR_Batching.thy

Extension-field transfer#

The assembly bound holds over the exact degree-four extension of KoalaBear, the denominator of the bound is exactly p^4, and four independent uniform base-field coefficients push forward to a uniform extension element. The executable challenge derivation is not part of the statement.

• Named theorems: gkr_assembly_soundness_ext4, ext4_denominator_exact, uniform_coeff_tuple_pushforward
• Canonical source: KoalaBear_Ext4_Nonsquare.thy, KoalaBear_Ext4_Field.thy, KoalaBear_Ext4_Lift.thy, KoalaBear_Ext4_GKR.thy

Two different objects are called degree four here. One is the per-variable degree bound inside the sumcheck; the other is the degree of the field extension.

Verifier acceptance refinement#

A successful acceptance trace of the shipped Rust verifier inhabits the reduction-chain event of the assembly result, given an explicit relation between the Rust trace values and the model. That relation is a stated premise. It is not discharged against the compiled program, so the result is a conditional refinement. The reverse direction is a stated non-claim.

• Named theorems: production_verifier_acceptance_refines_gkr_chain_bad, verifier_acceptance_implies_gkr_chain_bad, gkr_chain_bad_does_not_imply_public_input_acceptance
• Canonical source: Verifier_Acceptance_Refinement.thy

The model event does not mention the request and public-input guards. An inhabited model event therefore cannot authorize an executable acceptance whose public-input binding fails.

Concrete instances#

The compiler, composition and batching results have registered concrete instances over the production base field that fire their premises, so those theorems are not vacuously true. The extension-field result is an interpretation over the exact field, and the acceptance refinement's value relation is a premise that is not instantiated. The compiler and composition activations use a depth-one toy hash stack over KoalaBear. They show that the assumptions are satisfiable; they do not verify the full Poseidon2 implementation. The batching activation runs one accepting and one rejecting job.

How the Rust code is connected#

The Rust implementation is connected to the model in two ways.

Contracts. Creusot contracts, checked through Why3 with automated solvers, anchor selected code clauses to model clauses in four refinement scopes:

A further leaf-tag obligation requires the first field of every leaf preimage to remain the encoding tag in both the compiler and the primitive hash paths.

Acceptance refinement. The conditional theorem described above consumes an acceptance trace populated from the verifier's actual public-input, request-guard, zero-output, protocol-result and final input-claim observations. That trace is compiled only in the test and translation configurations. The ordinary build keeps the original short-circuit rejection form, and the equivalence of the two forms is part of the relation that is not discharged.

Read these boundaries with the evidence:

• A trusted annotation makes a function available to surrounding reasoning. It is not evidence that the function body was proved.
• Replay metadata does not replace checking the named source, assumptions and tool output.
• Two type-invariant leaves remain open and carry no claim: the mle_eval_base result type invariant and the shared verifier body's opaque derived-wiring entry type invariant.
• Value-level clauses that the current tools cannot check are recorded as documentation contracts inside the declared trust surface. They are not counted as machine-checked.

Trusted and assumed boundaries#

The formal evidence depends on:

• Isabelle/HOL and its code and document generation.
• The pinned Rust compiler and package graph.
• The Creusot and Why3 translation and the trusted annotations recorded in source.
• Field and hash implementations behind explicit abstract seams.
• An idealized challenge process for the whole interaction: once the transcript content so far is fixed, each four-coefficient tuple the challenger returns is jointly uniform over the base field and independent of every earlier tuple. This concerns the complete multi-round sequence, not one sample, and it is not established for the executable transcript.
• For any implementation-facing reading of the bound, a Fiat-Shamir reduction for this multi-round protocol, with its query-dependent and round-dependent loss. It would have to cover the exact duplex absorb-and-squeeze convention, the fixed message grammar and the concrete Poseidon2 permutation shared with the hash and the circuit commitment. The interactive bound does not transfer unchanged, and no such reduction is part of the repository.
• Correspondence between the model's fixed circuit-input values and the input vector the verifier derives from the submitted witness. The transcript absorbs the public inputs and the circuit commitment, not that witness-derived vector, so an implementation-facing argument must bind it before challenges are drawn or account for every witness an adversary tries.
• Correspondence between the modeled circuit and the selected Rust paths.
• The relation between the Rust trace values, the final running claim, the wiring right-hand side, the off-cube polynomial representation and the model, which the acceptance refinement carries as an undischarged premise.
• The fixed protected source identity for the published external proof.

The exact p^4 denominator belongs to the model bound, whose numerator and representation premises still apply. It is not an established error probability or bit-security level for the executable Fiat-Shamir verifier. The independent challenge-generation review (opens in a new tab) by Bernhard Müller (opens in a new tab) records the source-to-model path, the transcript schedule and these conditions.

Scope of the results#

• Compiled-Rust semantics and whole-program refinement.
• Fiat-Shamir soundness of the non-interactive verifier.
• The distribution of the executable's transcript-derived challenges.
• Correctness of the private wiring representation.
• The converse of the verifier acceptance refinement.
• An assembled end-to-end completeness theorem for a full protocol run. Completeness is mechanized for the compiler and at the layer-identity level.
• Zero knowledge or knowledge soundness. The core protocol has no zero-knowledge property, and the composition reasons from the absence of any valid witness, so it provides no extractor.
• Cryptographic security of the primitives, side-channel resistance, availability, deployment correctness and operational safety.
• Properties of receipt networks, destinations, custody, rollup proving, settlement or finality. The external proof identity and its receipt are implementation artifacts, not Isabelle theorems.

For how these limits affect an integration, see Trust boundaries.

Re-run the proofs#

Before you begin#

• Install Isabelle2025-2.
• Check out a copy of the Archive of Formal Proofs that contains the Sumcheck_Protocol entry, which GKR_Protocol extends.
• Plan for a long job. Five sessions declare a 7,200-second timeout and one declares 3,600 seconds, and a first build on a laptop takes a long time without being stuck.

Build the sessions#

From the root of the source repository, build the compiler session. It depends on GKR_Protocol, so this command builds both core sessions:

isabelle build -d /path/to/afp/thys -d formal/isabelle \
  SMT_Circuit_Compiler_Correctness

The four extension-field sessions form a chain on top of it. Building the last one builds all four:

isabelle build -d /path/to/afp/thys -d formal/isabelle \
  KoalaBear_Ext4_GKR

The pinned Isabelle2025-2 build rejects sorry under the default quick_and_dirty=false, and direct source scans provide an additional check for admitted or abandoned proofs. The generated PDFs under docs/ are base-session snapshots from 2026-08-29. They do not include the extension-field chain or the acceptance refinement; the theory sources do.

The hosted Proofs workflow rebuilds every registered session from clean targets when a pull request changes a proof input, on every push to the maintained branch and weekly. A session that does not complete fails the workflow, so a green result cannot come from a silently omitted session. The workflow does not rebuild the sessions on release events.

Run the Rust checks#

cargo fmt --all --check
cargo clippy --workspace --all-targets --locked -- -D warnings
cargo test --workspace --release --locked
cargo run --release --locked --bin proof_digest

The suites include positive, negative, differential, adversarial, codec and deterministic proof-digest checks. Release mode is required because the proving paths are impractically slow in a debug build. Passing tests do not prove the absence of untested defects.

If you change a proof input#

A change to a theory, a mapped Rust symbol, a contract, a theorem status, a protected source byte or a trusted boundary must update FORMAL_VERIFICATION.md and the relevant release manifest in the same reviewed change. Expected identity values are never regenerated to make changed source pass. See CONTRIBUTING.md (opens in a new tab) for the required checks.