Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

formal verification of blockchain software (authored by agents unless marked 🧑)

short version

  • the reviewed proof tools primarily check contract source or bytecode rather than validator clients
    • Certora Prover (Solidity, Rust/Solana), Move Prover (Aptos, Sui), Kontrol (Foundry tests on the K semantics of the EVM)
    • I found no published proof about any part of Agave or Firedancer, the two Solana validator clients
  • selected projects use LLMs to write specifications or proofs
    • EquiVM (below) proved 23 deployed Ethereum contracts in Lean, up to 100 million tokens and 100 hours each
    • Move and Solidity papers use LLMs to write specifications and use the prover as the judge
    • Certora and Aptos shipped agent products in 2025-2026
  • inference: specifications, assumptions, and proof soundness all need scrutiny
    • the Move bytecode verifier bug was in code nobody had proved
    • Certora’s Kamino report found bugs with proofs and a manual audit together
    • the Kamino proofs used a smaller number type and unrolled loops once
  • the reviewed Solana VM semantics and tests do not prove equivalence to the production VM code
    • an Isabelle model of sBPF (OOPSLA 2025) and a Lean port of it inside Solanalib
    • the safety theorem is about the model, tested against a reference VM
  • inference: the largest open piece is the bridge from these models to Agave and Firedancer code
  • best ideas
    • prove one small Agave piece, then compare the proof with Firedancer-Agave differential fuzzing at the same budget
    • measure how strong LLM-written specifications are, using real exploits and injected bugs
    • repeat EquiVM for deployed sBPF programs and price it

what the topic is

  • a smart contract is a program stored on a blockchain that moves money by rules
    • EVM (Ethereum): bytecode, usually compiled from Solidity
    • Move (Aptos, Sui): a language built around resources that cannot be copied
    • Solana: Rust programs compiled to sBPF bytecode, state kept in separate accounts
  • a validator client is the node software that orders transactions and runs them
    • it also contains the VM that runs the contracts
    • a bug in the VM or its verifier is a bug under every contract
  • three kinds of target, with different proof boundaries
    • the contract (often small and money-bearing; may be upgradeable)
      • proofs apply to a particular version
    • the VM and its bytecode checker (shared by all contracts)
    • the client (consensus, networking, storage, runtime), covered elsewhere

what existing work shows

solana programs and the solana vm

  • OtterSec, “Solana formal verification: a case study”
    • fact: industry blog, not peer reviewed
    • fact: Kani (bounded model checker) over Anchor programs, harnesses generated from succeeds_if and errors_if annotations
    • fact: applied to the Squads multisig, proving threshold validity (≥1 and ≤ member count) and member requirements
    • fact: they swapped in cheaper types (4-byte pubkeys, fixed arrays) to avoid path explosion
    • limit (fact, their list): cross-program calls and custom serialization stay hard, runtime and consensus out of scope
    • inference: the proof is about a modified SDK, so the gap to the real SDK is a trusted step
  • Certora Solana Prover docs
    • fact: vendor documentation, not peer reviewed
    • fact: rules are written in CVLR, “an embedded DSL that lives in two crates”
    • claim (Certora blog, seen as search snippet): the tool analyzes SBF bytecode, so the compiler is not trusted
    • not opened: the 2023 Certora posts on the Solana tool
  • Certora, Kamino Vault report, 2025
    • fact: vendor audit report, work Jan to Jun 2025 in three rounds
    • fact: quote, “the Certora Prover demonstrated that the implementation of the Solana contracts above is correct (modulo identified issues) with respect to the formal properties formulated and written by the Certora team”
    • fact: findings: 0 high, 3 medium, 2 low confirmed and fixed in the summary table, plus informational ones
    • fact: assumptions section: fixed-point numbers shrunk from FixedU128<60> to FixedU64<14> “for tractability”, loops unrolled once (“a loop_iter of 1”)
    • fact: the 5 written properties include vault solvency and give_up_pending_fees does not revert
    • inference: this is the best public picture of what a Solana proof engagement looks like, and the proved claim is smaller than “the program is correct”
  • Yuan et al., “A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana”, OOPSLA 2025
    • fact: peer reviewed, abstract page read, paper itself not opened
    • fact: claims “the first and most comprehensive formal semantics” of Solana’s eBPF, small-step, in Isabelle/HOL
    • fact: they extract an executable semantics and test it against the original interpreter
  • Solanalib (Solana Foundation, Lean 4)
    • fact: experimental repository; README checked directly October 8, 2026
    • fact: six layers (primitives, numbers, accounts, instructions, finance, sBPF)
    • claim: sBPF layer is “a Lean port of the OOPSLA 2025 Isabelle/HOL formalisation”, validated against a reference VM
    • limit: the current README does not substantiate the earlier draft’s test counts or theorem counts
    • fact: models specification layers and the sBPF instruction set
      • README describes the bytecode-to-protocol proof chain as an eventual goal
    • inference: this is a proof about a model of sBPF, so it does not yet say anything about Agave’s Rust sBPF code or Firedancer’s C code
  • Cloosters et al., SseRex, DIMVA 2026
    • fact: peer reviewed venue per the arXiv page, symbolic execution (not a proof)
    • fact: finds missing owner, signer, and key checks and arbitrary cross-program calls in sBPF lifted to an IR
    • fact: 8,714 bytecode-only contracts, 467 flagged; of a sample of 30 reports, 26 were true bugs (87%)
    • fact: motivating quote: “Unlike the Linux kernel’s eBPF, it lacks the control-flow verification mechanism”
    • inference: the Solana-specific bug classes are all account-checking rules, which is a good fit for proofs over small rule sets
  • firedancer-io/solana-conformance
    • fact: README, archived 16 April 2026
    • fact: compares Firedancer to Agave on harnesses including ELF loader, VM interpreter, VM validate, syscalls, transactions, blocks
    • inference: the current assurance that Firedancer and Agave agree is differential testing, not proof
    • not opened: the solfuzz-agave repository and any bug counts

move: prover, specifications, and the verifier bug

  • Dill et al., “Fast and Reliable Formal Verification of Smart Contracts with the Move Prover”
    • fact: arXiv v3 Feb 2022; I did not confirm the venue, so treat peer review as unconfirmed
    • fact: claim, quote: “The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes”
    • fact: key choices: alias-free memory model, fine-grained invariant checking, monomorphization
    • limit: Diem is gone, and the Prover trusts its Boogie/SMT stack and the Move semantics it encodes
  • Grieskamp et al., “Formal Verification of Imperative First-Class Functions in Move”, FMCAD 2026
    • fact: peer reviewed
    • fact: adds “behavioral predicates” and “state labels” so specs can talk about function values that are only known at run time
    • fact: also describes spec inference by weakest-precondition analysis
    • inference: dynamic dispatch is what makes smart contracts harder to verify, and Aptos paid for it in prover work
  • Fu, Xu, Kim, “Agentic Specification Generator for Move Programs” (MSG), ASE 2025
    • fact: peer reviewed (ASE 2025 per arXiv page), supported by the Sui Foundation
    • fact: quote: “successfully generates verifiable specifications for 84% of tested Move functions”
    • fact: the agentic split gave “57% more verifiable clauses”, prover feedback gave “a 30% increase”
    • fact: evaluated on move-stdlib (10 functions), aptos-stdlib, and aptos-framework (242 of 284 covered), compared with expert-written specs
    • limit: “verifiable” means the Prover accepts the clauses, not that they are strong; the paper compares to expert specs by match
    • inference: the weak-spec risk is the main open question, see the gaps
  • Grieskamp, Zhang, Kashyap, “Combining Mechanical and Agentic Specification Inference for Move”, arXiv 2026
    • fact: preprint, self-described “early work”, tools paper with preliminary results
    • fact: weakest-precondition analysis on Move bytecode gives a sound base; Claude Code through an MCP server fills in loop invariants; the Prover judges
    • fact: quote: “the AI is used precisely where WP is weakest”
    • limit: tried on canonical library examples, no benchmark numbers
  • Sui Prover blog (Asymptotic)
    • fact: vendor blog, no evaluation, no comparison to the Aptos prover
  • Zellic, “The Billion Dollar Move Bug”
    • fact: security blog, not peer reviewed; page checked directly October 8, 2026
    • fact: a control-flow-graph bug in the shared move-binary-format crate: “The very last opcode in a function with 65,534 instructions will always have no successors”
    • fact: introduced 6 October 2022, fixed 30 March 2023; affected Sui and Aptos; no public exploitation reported
    • inference: the verifier is the thing that makes Move’s type and reference safety true, and no formal proof of it appears in what I read

evm and solidity: tools and semantics

lean and llm proofs of bytecode

  • Lazaropoulos and Paraskevopoulou, “Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens” (EquiVM), arXiv 2026
    • fact: preprint, full text read
    • fact: Lean semantics for EVM plus a spec language (“Sol−”); the theorem says deployed bytecode refines the spec for any state, calldata, and gas, or runs out of gas
    • fact: 23 contracts proved, “most of the MakerDAO stablecoin system”; two (Clipper, Auction) unfinished at 26/29 and 18/20 functions
    • fact: table 2: for example Vat took 100h 44m and 74.8M tokens, and Spot 5h 47m and 5.7M tokens; the abstract says up to 100 million tokens and 100 hours
    • fact: cost: pricing the largest run at gpt-5.5 list prices gives “roughly 150,000 at API rates”
    • claim: humans did not read or write its code, but it was “nowhere close to a fully automated effort”
    • fact: authors call it pre-alpha and expect “subtle gaps in the formal verification”
  • evmSmith (Lean, on top of EVMYulLean)
    • fact: repository page, updated 30 September 2026, “fails to build on Lean v4.22.0”
    • fact: three examples including WETH solvency; partial correctness only, failure paths vacuous
  • Ethereum Magicians, “Optimized Verified EVM Interpreters for ZK”
    • fact: forum proposal, “we do not have concrete plans yet”; builds on rocq-of-rust for Revm and a RISC-V assembly route
  • not opened: Verity (EVM language with a verified compiler, only seen cited inside the EquiVM paper)

llm help for finding properties and bugs in solidity

  • Liu et al., PropertyGPT, NDSS 2025
    • fact: peer reviewed; GPT-4 with retrieval over human-written Certora properties, then compile and prove loop
    • fact: “80% recall compared to the ground truth”, 26 of 37 CVEs/incidents, 12 zero-days, 550.1M simulated; on contracts exploited after the knowledge cutoffs, $4.6M
    • claim: quote, “the same agents capable of exploiting vulnerabilities can also be deployed to patch them”
    • inference: attackers get the same cost drop that makes proofs cheaper, so unproved code faces cheap search

llm products and consensus proofs

zk and zkvm code under ethereum

what is missing

  • this review did not find proof about Agave or Firedancer code
    • evidence: searches for Kani, Verus, Lean, or Isabelle together with Agave, Firedancer, or sBPF found only Solanalib and the OOPSLA Isabelle model (both models of sBPF) and the Certora and OtterSec contract tools
    • the human’s Agave sizing is the only sizing I found
  • this review did not find proof linking Solanalib’s sBPF model to the real VM code
    • differential testing is the only link in the README
  • this review did not find formal proof of the Move bytecode verifier in what I read
    • evidence: the Zellic bug sat in the CFG builder it depends on
  • this review did not find measurement of how strong LLM-written specs are on Solana or Move
    • MSG measures “verifiable” and match to experts, PropertyGPT measures recall against human properties
    • Monperrus’ 28 exploits are the closest ready benchmark, but only for Ethereum and only for tools that make invariants
  • this review did not find public cost data for Solana proofs
    • EquiVM has token and hour tables for Ethereum, the Solana side has Certora engagement dates only
  • this review did not find study of drift
    • the inspected sources do not measure how often proved Solana or Move code is upgraded without re-proof
  • this review did not find comparison of proofs and differential fuzzing for client code
    • the Firedancer conformance suite exists but its bug yield was not opened

research we can do

idea 1: proof versus differential fuzzing on one agave piece

  • question
    • if we prove the compute-budget instruction sanitizer, does the proof find divergences from Firedancer that Agave-Firedancer fuzzing missed?
  • builds on
  • what is new
    • an equal-budget comparison of a proof and fuzzing on a real validator pair
  • why it matters
    • tells validator teams which of the two to buy first
  • first experiment
    • write the spec independently of the code, prove Agave’s Rust against it, run the same spec as an oracle on Firedancer’s C by test
    • give fuzzing the same engineer-weeks
  • convincing result
    • either an input only the proof or the oracle finds, or a clear statement that neither found anything and what each cost
  • cost
    • 5-8 engineer-weeks from the sizing note, plus the C-side harness
  • closest work that could scoop it
    • Anza or Firedancer teams doing the same internally; no public version found

idea 2: how strong are llm-written specs, measured by real exploits

  • question
    • do specifications from MSG-style or AutoProver-style generators fail on the real exploit, or just verify cleanly?
  • builds on
  • what is new
    • a strength measure, not a “verifies” rate; spec mutation plus exploit replay
  • first experiment
    • generate rules from intended behavior or patched code
    • on vulnerable code, record proof failures, checked counterexamples, and exploit violations separately
      • soundly proved rules cannot be violated by an execution covered by the proof
    • also inject bugs of the Kamino kind (rounding, first depositor) into a verified vault and count what survives
  • convincing result
    • a table of generated-spec kill rate against human-spec kill rate on the same bugs, with the 2 of 28 baseline for invariant tools
  • cost
    • a few weeks and model tokens; Certora access for the Solidity side
  • scoop risk
    • Certora (AutoProver evaluation), the Monperrus group follow-up

idea 3: equivm for deployed sbpf programs

  • question
    • can an LLM agent produce a Lean refinement proof for a deployed Solana program, and at what token cost?
  • builds on
  • what is new
    • first token and hour numbers on Solana, and a first test of whether Solanalib’s model is good enough to prove against
  • first experiment
    • pick the Address Lookup Table state views (119 production lines), compile, state the property from the Agave note, let an agent prove it on the bytecode
  • convincing result
    • a complete proof plus a list of every semantic hole the agent hit, like EquiVM’s array wrap-around
  • cost
    • unknown; account models exist, but the proposed program’s syscalls and transaction behavior need a separate coverage audit
  • scoop risk
    • the EquiVM authors, Certora, or the Solana Foundation extending Solanalib

what i searched

  • web search, standard and extended
    • Move Prover, Sui Prover, Aptos AI verification
    • Certora, AutoProver, Solana Prover, Kamino, Kontrol, Halmos
    • Solana, sBPF, rbpf, Agave, Firedancer with Kani, Verus, Lean, Isabelle
    • Ethereum clients, EVM semantics in Lean, Isabelle, Dafny, Rocq
    • verified zkEVM, OpenVM, SP1, Alpenglow proofs
    • LLM plus Solidity verification, 2025 and 2026
  • opened about 35 sources, about 12 as full text
    • full text: EquiVM, MSG, Move spec inference, FMCAD Move, Move Prover, LLM oracles, SseRex, Neuroforger, invariants paper, IsabeLLM, PropertyGPT, Mota 2023, Kamino report
    • paper-collection additions: those papers except the Mota paper and the Kamino report
  • not covered
    • KEVM and K papers, Halmos, SMTChecker papers, Tezos, Cardano, Algorand, Cosmos SDK, Bitcoin Script
    • Alpenglow proofs: the search returned none, so I cannot say none exist
    • Solana client bugs and their classes (CVE data), Firedancer’s own fuzzing results
    • ChatGPT was unavailable and was not consulted
  • limits
    • publication review checked Zellic, Solidus, Solanalib, and the SP1 blog directly
      • removed Solanalib counts absent from its current README
    • the Move Prover TACAS venue and the Verity compiler were not confirmed from a primary source

Last edited: