Lean4 + Formal Verification: A Mental Model for the gean Team

# Lean4 + Formal Verification: A Mental Model for the gean Team > A pre-learning document. The goal is **conceptual scaffolding** — to give you a complete mental model of formal verification, Lean4, and how they fit into Lean Ethereum's roadmap before you write a single line of Lean. There is no Lean4 code in this document on purpose. > > **Audience**: a gean contributor who knows Go, knows the consensus protocol they're implementing, and is now expected to become the team's resident "Lean4 person" because the EF formal verification timeline ends at the consensus client layer in 2027. > > **Reading time**: 60–90 minutes. Designed to be read once cover-to-cover, then revisited as a reference. --- ## Table of contents - [Part I — Framing: the two-domain confusion](#part-i--framing-the-two-domain-confusion) - [Part II — Formal verification, from scratch](#part-ii--formal-verification-from-scratch) - [Part III — The other "proof" word: arguments of knowledge](#part-iii--the-other-proof-word-arguments-of-knowledge) - [Part IV — Lean4, specifically](#part-iv--lean4-specifically) - [Part V — Prerequisites: what to learn before opening Lean4](#part-v--prerequisites-what-to-learn-before-opening-lean4) - [Part VI — Learning Lean4: a phased curriculum](#part-vi--learning-lean4-a-phased-curriculum) - [Part VII — How Lean4 will (and will not) integrate with gean](#part-vii--how-lean4-will-and-will-not-integrate-with-gean) - [Part VIII — Where Lean4 specifically helps gean](#part-viii--where-lean4-specifically-helps-gean) - [Part IX — Becoming the team's Lean4 person](#part-ix--becoming-the-teams-lean4-person) - [Part X — Quick reference: glossary, links, action checklist](#part-x--quick-reference-glossary-links-action-checklist) --- # Part I — Framing: the two-domain confusion ## 1. Why this document exists If you walk into a room of cryptographers and Ethereum researchers and say the word **"proof"**, half the room hears one thing and half hears another. This is the single biggest source of confusion in everything you are about to learn, so we will deal with it before anything else. There are **two completely different things** both called "proof" in the lean Ethereum world: 1. **Formal verification proofs** — mathematical proofs *about programs*, written in a proof assistant like Lean4, checked by a small kernel. These prove statements like "this fork choice algorithm cannot select a block that is not an ancestor of the head". They look like a mathematician's chalkboard. 2. **Cryptographic argument-of-knowledge proofs** (ARK / NARK / SNARK / STARK) — short binary blobs produced by a *prover* and checked by a *verifier* that convince you the prover knows some secret or that some computation was done correctly, *without* re-running the computation. They look like a few kilobytes of bytes. These are unrelated concepts that share a word. | Aspect | Formal verification (Lean4) | Cryptographic argument (SNARK) | |---|---|---| | What is being proved | A property of a program / spec | Knowledge of a witness / correctness of a computation | | Who reads the proof | A computer (the proof kernel) | A computer (the verifier) | | When | Once, at development time | At runtime, every time | | Output | A `.lean` file the kernel checks | A few kB of bytes | | Trusted by | The kernel + Mathlib axioms | Cryptographic hardness assumptions | | Failure mode | Compile error | Rejected proof or soundness break | | Example in gean | (none yet) | `xmss/rust/multisig-glue` produces these every block | The one-line distinction: > **Lean4 proves things about programs. SNARKs prove things about secrets.** They meet in exactly one place: the **ArkLib** project, which uses Lean4 (formal verification) to write down and prove the security of SNARK protocols. ArkLib is the hinge of this entire document because it is the bridge between the two worlds, and because the WHIR-based aggregation that gean already uses (`xmss/rust/multisig-glue/src/lib.rs`) is on ArkLib's roadmap. If you remember nothing else from Part I, remember the table above and the one-line distinction. ## 2. The map Here is where everything you are about to learn fits: ``` ┌──────────────────────────────────────────────────────────────────────┐ │ MATH & LOGIC │ │ (set theory, type theory, abstract algebra, probability) │ └────────────────────────────┬─────────────────────────────────────────┘ │ ┌──────────────┴──────────────┐ ▼ ▼ ┌─────────────────────┐ ┌─────────────────────────┐ │ PROOF ASSISTANTS │ │ CRYPTOGRAPHIC PROOFS │ │ (Lean4, Coq, │ │ (interactive proofs, │ │ Isabelle, Agda) │ │ Σ-protocols) │ └──────────┬──────────┘ └────────────┬────────────┘ │ │ ▼ ▼ ┌─────────────────────┐ ┌─────────────────────────┐ │ MATHLIB │ │ ARK / NARK / SNARK / │ │ (formalized math, │ │ STARK │ │ ~1.6M LOC) │ │ (FRI, WHIR, BaseFold, │ │ │ │ Sum-Check, Spartan) │ └──────────┬──────────┘ └────────────┬────────────┘ │ │ └──────────────┬────────────────┘ ▼ ┌──────────────────────────────┐ │ ArkLib │ │ Lean4 library of formally │ │ verified SNARK protocols │ │ (Quang Dao, CMU) │ └──────────────┬───────────────┘ │ ┌──────────────┼──────────────┐ ▼ ▼ ▼ ┌──────────┐ ┌─────────────┐ ┌────────────┐ │ Lean-EVM │ │ Verified │ │ VERIFIED │ │(Nethermind│ │ zkVM │ │ CONSENSUS │ │ Lean4) │ │ circuits │ │ (target: │ │ │ │ │ │ end-2027) │ └──────────┘ └─────────────┘ └─────┬──────┘ │ ▼ ┌────────────────────────┐ │ gean / ream / zeam │ │ ethlambda / qlean │ │ (Go / Rust / Zig / │ │ C++ / etc.) │ └────────────────────────┘ ``` **Where gean sits today**: nowhere on this diagram. It is a Go consensus client that does not import or interact with Lean4 in any way. The only "proof" it touches today is the SNARK from `multisig-glue` — and that proof's *correctness* has not been formally verified in Lean4 yet either. **Where gean will sit by end-2027**: in the consensus box at the bottom. The Ethereum Foundation's snarkification team (Alex Hicks) has explicitly listed *consensus specs and implementations* as the 2027 deliverable for the verified zkEVM project. That is the target gean is implicitly committed to. **Your job**: build the human bridge between gean (the bottom of the diagram) and Lean4 (the top). Nobody does this *for* a client — the client team has to grow the expertise itself. ## 3. The vocabulary trap, in detail A few more terminology landmines worth defusing now, because you will hit all of these in the first week: - **"Lean Ethereum"** — the post-quantum consensus rebuild (also called Beam Chain). *Has nothing to do with Lean4* the language. The names collide; ignore the collision. "Lean" here means *minimal*, *small*, *trim*, in the sense of "a lean codebase". This is why we call the spec **leanSpec**, the signature library **leanSig**, the zkVM **leanVM**, and the multisig stack **leanMultisig** — and *none* of those are Lean4 code. They are all written in Python or Rust. - **"leanSpec"** — the executable Python reference specification of the Lean Ethereum protocol (`/Users/bankat/Documents/protocol/gean-agent/leanSpec/`). This is the *target* that a future Lean4 spec might be ported from, but it is *not* itself a Lean4 spec. Today it is Python + Pydantic + SSZ. - **"leanSig"** — the Rust library for hash-based post-quantum signatures (`/Users/bankat/Documents/protocol/gean-agent/leanSig/`). It is the cryptographic primitive layer. Not Lean4. The "lean" in the name is the same "lean" as in Lean Ethereum. - **"Lean-EVM"** — *this one actually is Lean4*. It is Nethermind's formal Lean4 specification of the Ethereum Virtual Machine. It has nothing to do with leanSpec, leanSig, or leanVM, but the naming overlap is brutal. When you read "Lean-EVM" in a workshop note, mentally translate it as "the Lean4 EVM model". - **"leanVM"** — a *minimal zkVM* for post-quantum signature aggregation, designed by Thomas Coratger and Emile (EF). Written in Rust and a custom DSL. Not Lean4. Same naming gotcha. - **"ArkLib"** — Quang Dao's Lean4 library for formally verifying SNARKs. The "Ark" stands for **Arguments of Knowledge**, the cryptographic concept (not Apache Arrow, not Noah's ark, not the Rust crate). ArkLib *is* Lean4. - **"Mathlib"** or **"Mathlib4"** — the community-maintained library of formalized mathematics in Lean4. ~1.6 million lines of formal math. This is where every serious Lean4 project lives. If you build a mental rule of thumb, it is this: > **The word "lean" in lean Ethereum almost never refers to Lean4 the language. The two exceptions are "Lean-EVM" and "ArkLib in Lean".** Memorize this and you will save yourself a week of confusion. --- # Part II — Formal verification, from scratch ## 4. What "formal" means In ordinary English, "formal" means dressed up. In computer science it means **the opposite of empirical**. When you write a unit test, you are doing **empirical** verification: you run the program on some inputs, observe the outputs, and conclude that the program *probably* works on inputs you have not tried. You are sampling. When you do **formal** verification, you do not run the program at all. You write down a mathematical statement about *all possible inputs* — for example, "for any block B and any state S, if B's parent root matches S's latest header, then ProcessBlock(S, B) returns a state whose latest header equals B" — and you construct a proof that the statement is true. The proof is checked symbolically by a small program (the *kernel*) that mechanically follows logical rules. The difference matters because: - **Tests sample.** Even 100% line coverage tests only the *paths the test suite happened to think of*. The Therac-25 medical device had millions of treatment runs before its race condition killed someone. - **Proofs cover everything.** A successful Lean4 proof of a theorem about `ProcessBlock` covers *every* possible state and *every* possible block, including the ones you never imagined. - **Proofs are also not magic.** They prove only what the theorem statement says. If you state the wrong theorem, the proof is worthless. The hardest part of formal verification is *writing the right theorems*, not proving them. ## 5. Soundness and completeness These two words appear constantly. Define them now. - A verification system is **sound** if every statement it accepts as proved is *actually true*. Soundness is the non-negotiable property. An unsound system is worse than no system, because it gives false confidence. - A verification system is **complete** if every true statement *can* be proved in it. By Gödel's incompleteness theorems, no rich-enough system is both sound and complete. Lean4 is sound but not complete. (This rarely bites you in practice.) When ArkLib's authors say they prove "round-by-round knowledge soundness" of an Interactive Oracle Reduction, they are using *both* meanings of "soundness": the cryptographic soundness of the protocol *and* the Lean4 (formal verification) soundness of their proof. ## 6. Models versus implementations Formal verification always involves a **model** of the thing you care about, not the thing itself. You cannot directly prove things about gean's compiled binary. You can only prove things about a *model* of gean — for example, a Lean4 function that *describes what the binary is supposed to do*. The gap between model and implementation is real and must be bridged somehow. The bridges are: - **Conformance testing.** The implementation passes the same tests as the model. (gean already does this with `spectests/` against the leanSpec Python reference.) - **Code extraction.** The model *is* the code: write the function in Lean4, prove it, then extract it to Rust/C/Go. Lean4 has reasonable extraction to C and to a Lean-native runtime; extraction to Rust/Go is an open research problem. - **Refinement proofs.** Formally prove that the implementation refines the model, in the sense of one being a "more concrete" version of the other. This is heavy and rarely done end-to-end for whole programs. - **Translation validation.** For each compilation, prove that the compiled code matches the source. Not done for production today. In practice, every real-world FV project picks **one** of these bridges and accepts that the others are gaps. The gap is part of the *trusted computing base* (TCB) — the things you have to trust to trust the proof. ## 7. Hoare logic in five minutes Almost all program verification is built on **Hoare logic**, named after Tony Hoare. The basic idea is to write annotations of the form: ``` { P } command { Q } ``` Read this as "if proposition P is true before `command` runs, and `command` terminates, then proposition Q is true after". `P` is the **precondition**, `Q` is the **postcondition**. For loops, you also need a **loop invariant** — a proposition that is true *before* the loop, *after each iteration*, and therefore *at the end*. The whole game of verifying a loop is finding the right invariant. Concretely, in gean's `forkchoice/protoarray.go`, an invariant for the proto-array tree might be: *"at every point, every node's score equals the sum of attestation weights for that node's subtree"*. If that invariant holds before applying a vote delta and after, and you can prove that `ApplyScoreChanges` preserves it, then you have proved a global property of the entire fork choice without ever running it. You do not need to be fluent in Hoare logic to read this document. You just need to recognize the words **precondition**, **postcondition**, and **invariant** when they appear in workshop notes. They are the bread and butter of every FV conversation. ## 8. Refinement and state machines Most of consensus is naturally modeled as a **state machine**: the state is `BeaconState`, the transitions are slot processing, block processing, attestation processing. A **refinement** is a relationship between two state machines where one is "more concrete" than the other. A high-level spec might say "after a valid block, the state's latest header is the new block's header". A more concrete spec might say "after a valid block, `state.LatestBlockHeader` is updated, then `state.HistoricalBlockHashes` is appended to, then the slot bitlist is rotated". A refinement proof shows that *every behavior of the concrete machine corresponds to a behavior of the abstract machine*. This is the right framing for thinking about gean ↔ leanSpec ↔ a future Lean4 spec. Each layer is a refinement of the one above. ## 9. Why testing is not enough for consensus Three concrete reasons specific to gean: 1. **Tiebreakers in fork choice are adversarial.** The 32-byte lexicographic tiebreaker in `forkchoice/spec.go:rootGreaterThan` exists precisely to make fork choice deterministic across clients. A bug in the tiebreaker shows up only when two equal-weight blocks share a parent — a 1-in-2^256 condition that no fuzzer will hit randomly, but that an adversary will deliberately engineer to cause a chain split. The only way to be sure is to *prove* that the tiebreaker is total, antisymmetric, and consistent across all clients. 2. **Justification rules are number-theoretic.** Look at `gean/statetransition/justifiable.go`. The 3SF-mini rule says a slot can be justified after the finalized slot if the distance is **≤5**, **a perfect square**, or **a pronic number** (n·(n+1)). Bug-finding here is not "is the test green?" — it is "are perfect squares and pronic numbers correctly characterized for all `delta` up to 2^64?". The function uses `math.Sqrt` on a `uint64` cast to `float64`, which loses precision for large deltas. *Is the function correct on the boundary?* You can write a Lean4 proof that says it is, or you can wait for someone to find the edge case in the wild. 3. **Finalization invariants are global.** A bug in fork choice that lets the head temporarily diverge from the finalized chain is a *liveness* bug today and a *safety* bug tomorrow. Liveness bugs are not catchable by unit tests at all, because they involve sequences of events stretched over time. They are catchable by *invariant proofs*: state an invariant of the form "at every point, the head is a descendant of the finalized root", and prove it is preserved by every transition. These three failure modes — adversarial inputs, number-theoretic edge cases, and liveness invariants — are the headline reason consensus clients are good FV targets. They are also the failure modes that destroyed real projects (DAO fork, Medalla, Kiln). ## 10. What a proof assistant actually is A proof assistant is a programming environment where the program you write **is** a proof. When you finish writing it and the type-checker accepts it, you have a proof. The architecture of every modern proof assistant has the same shape: ``` ┌──────────────────────┐ │ User code │ │ (theorems, tactics, │ │ definitions) │ └──────────┬───────────┘ │ ▼ ┌──────────────────────┐ │ Elaborator / parser │ │ (Lean 4 has a very │ │ sophisticated one) │ └──────────┬───────────┘ │ ▼ ┌──────────────────────┐ │ Type-checking │ │ KERNEL │ ◄── this is the trusted computing base. │ (small, audited, │ everything else can be wrong. │ rarely changes) │ └──────────────────────┘ ``` The **kernel** is small (a few thousand lines for Lean4) and is the only thing you have to trust. Everything else — tactics, automation, the elaborator, the IDE, even the Lean compiler — can have bugs without compromising soundness, because every proof you produce ultimately gets re-checked by the kernel against the unchanged rules of dependent type theory. This is why people say things like "the trusted computing base of a Lean4 proof is the kernel plus the axioms used". It is literally true: nothing else can produce a false positive. ## 11. Interactive vs automated theorem provers Two big families: - **Interactive theorem provers (ITPs)**: Lean4, Coq, Isabelle, Agda. The user writes the proof step by step, with tactics and automation helping. Suitable for proving rich, deep theorems (e.g., the four-color theorem, the odd order theorem, the security of WHIR). You drive; the tool checks. - **Automated theorem provers (ATPs)**: SMT solvers like Z3, CVC5, and Boolector. Push-button: you state a logical formula, the tool says SAT / UNSAT / UNKNOWN. Good for decidable fragments (linear arithmetic, bitvectors, arrays). Useless on rich math. Modern Lean4 work uses **both**: write the high-level proof in Lean4 with tactics, dispatch the boring arithmetic obligations to an SMT solver via `polyrith`, `linarith`, `omega`, or external bridges. Alex Hicks' talk explicitly mentions "Lean and SMT solvers integrated in CI" as part of the zkVM track. For consensus client work, ITP-driven (Lean4) is almost certainly the right choice because the theorems are *structural* (state machines, refinement, invariants), not arithmetic. ## 12. A comparison table of proof assistants and SMT Treat this as a quick reference. You do not need to learn any of these except Lean4. | Tool | Logic | Strengths | Used by lean Ethereum? | |---|---|---|---| | **Lean4** | Dependent type theory (CIC variant) | Modern syntax, growing ecosystem, Mathlib, tactic framework, decent automation, used by EF | **Yes — primary tool** | | **Coq** | Calculus of Inductive Constructions | Mature, OCaml-style, *Software Foundations* textbook, CompCert | Some legacy (verified compilers history), not the EF choice | | **Isabelle/HOL** | Higher-order logic | Extremely mature, best for classical math, AFP archive | Niche; not used here | | **Agda** | Dependent type theory | Very pretty, used in academia for semantics | Niche; not used here | | **F\*** | Refinement types + SMT | Verified TLS (HACL\*), automated, less manual | Adjacent (HACL\* is referenced for crypto verification) | | **Z3 / CVC5** | First-order logic with theories | Push-button, decidable fragments, fast | Used as backend, not primary | The reason Lean4 is the EF choice is a combination of: - **Mathlib momentum**: Lean4 has by far the most active formalized math community. Every cryptographic proof you would want to write builds on facts from algebra, number theory, probability, and analysis — all of which live in Mathlib4. - **The snarkification team picked it**: Alex Hicks' verified zkEVM project (`https://verified-zkevm.org/`) standardized on Lean4 for the cryptography track. - **ArkLib already exists in Lean4**: switching languages would mean rewriting Quang Dao's work. - **Lean-EVM is in Lean4**: Nethermind's Ethereum Virtual Machine model is in Lean4 and passes 99.99% of conformance tests. These facts together create network effects. Lean4 won this corner of the market by 2024–2025. --- # Part III — The other "proof" word: arguments of knowledge ## 13. The cryptographic meaning of "proof" In cryptography, a **proof** is a protocol — a conversation between two parties — at the end of which one party (the *verifier*) is convinced of some statement. The party doing the convincing is the *prover*. The simplest kind is a **proof of knowledge**: the prover convinces the verifier that they know some secret (a discrete log, a preimage of a hash, a satisfying assignment to a circuit) without revealing the secret. The classic textbook example is Schnorr's identification protocol. Three properties characterize these protocols: - **Completeness**: an honest prover with the secret always succeeds. - **Soundness**: a cheating prover without the secret fails (with high probability). - **Zero-knowledge** (optional): the verifier learns *nothing* about the secret beyond the fact that it exists. The first two are mandatory. The third (zero-knowledge) is optional and only relevant when the witness is private. ## 14. Interactive proofs and Fiat-Shamir The earliest argument systems were **interactive**: the prover and verifier exchange messages back and forth, the verifier sends random challenges, the prover responds. Schnorr's protocol is three messages. Interactivity is annoying in practice. You want to be able to *generate a proof* and *send it to anyone* without holding a live connection. The **Fiat-Shamir transform** turns any interactive proof into a non-interactive one by replacing the verifier's random challenges with the output of a hash function applied to the protocol transcript so far. The prover hashes everything they have said and uses the hash as the "challenge" the verifier would have asked. Fiat-Shamir is the universal NI-fication procedure. Every NARK / SNARK / STARK in production today is a Fiat-Shamir-transformed interactive protocol. ArkLib formalizes the transform itself (the "BCS" component) and then formalizes the underlying interactive protocols separately. ## 15. ARK / NARK / SNARK / STARK — precise definitions This is the section the user explicitly asked for. Be precise. - **ARK** = **Argument of Knowledge**. - "Argument" (as opposed to "proof"): the soundness holds only against *computationally bounded* adversaries. A computationally unbounded prover could fool the verifier. In practice, all real systems are arguments, not "proofs of knowledge", because they rely on cryptographic hardness assumptions. - "Of knowledge": the prover convinces the verifier that they *know* a witness (not just that one *exists*). This is stronger than a plain argument. - Plain ARKs are **interactive**. - **NARK** = **Non-interactive Argument of Knowledge**. - Same as ARK but without the back-and-forth — typically obtained by Fiat-Shamir. - The proof is a single message from prover to verifier. - **SNARK** = **Succinct Non-interactive Argument of Knowledge**. - "Succinct" means the proof size and the verifier's running time are *sublinear* in the size of the statement being proved (often *polylogarithmic* or even *constant*). - This is the property that makes SNARKs practical for blockchains: you can verify the result of a huge computation by checking a tiny proof. - Examples: Groth16, PLONK, Marlin, Spartan, Halo2, Plonky2, Plonky3, **WHIR**, BaseFold, FRI-based systems. - **STARK** = **Scalable Transparent Argument of Knowledge**. - "Scalable": prover time scales quasi-linearly with the computation. - "Transparent": no trusted setup. (This matters because trusted setup ceremonies are operationally painful and politically risky.) - STARKs are typically post-quantum secure because they rely on hash functions and coding theory rather than elliptic curves. Most STARKs are also SNARKs (succinct), so the categories overlap heavily. - Examples: ethSTARK, Plonky2 (Plonky2 is both a STARK and a SNARK), Stwo, **WHIR**. The relationships visually: ``` ┌──────────────────────────┐ │ ARK │ │ (interactive, sound vs │ │ bounded adversaries) │ └────────────┬─────────────┘ │ + Fiat-Shamir ▼ ┌──────────────────────────┐ │ NARK │ │ (non-interactive) │ └────────────┬─────────────┘ │ + succinctness ▼ ┌──────────────────────────┐ │ SNARK │ │ (succinct, NI) │ └────┬────────────────┬────┘ │ │ + transparent │ │ + (often) setup + │ │ pairing-based post-quantum │ │ ▼ ▼ ┌────────────────┐ ┌───────────────────┐ │ STARK │ │ pairing SNARKs │ │ (FRI, WHIR, │ │ (Groth16, PLONK, │ │ BaseFold, │ │ Marlin) │ │ ethSTARK) │ │ │ └────────────────┘ └───────────────────┘ ``` A comparison table for the road: | Property | Σ-protocol | Groth16 | PLONK | STARK / WHIR | |---|---|---|---|---| | Interactive | Yes | No (after FS) | No (after FS) | No (after FS) | | Trusted setup | None | Per-circuit | Universal | None | | Proof size | ~kB | ~200 B | ~500 B | ~50–200 kB | | Verifier time | ms | ms | ms | ms–s | | Prover time | ms | s | s | s | | Post-quantum | If based on hashes | No (pairings) | No (pairings) | Yes | | Used by gean? | No | No | No | **Yes (WHIR)** | The thing to understand for gean specifically: lean Ethereum chose **WHIR** (a hash-based STARK / SNARK) precisely because of the post-quantum and transparent-setup properties. You see this choice all over the codebase: `xmss/rust/multisig-glue/Cargo.toml` depends on `whir_p3` and `KoalaBear` (the field). The `xmss_aggregate` function takes thousands of XMSS signatures and outputs a single WHIR proof that all of them verify under a known public key set. ## 16. Where these proofs live in gean today Concretely, in the codebase you already have: - `gean/xmss/rust/multisig-glue/src/lib.rs` — the Rust crate that wraps `rec_aggregation::xmss_aggregate`. This is the SNARK prover. It produces a `Devnet2XmssAggregateSignature` from a list of public keys, signatures, message hash, and epoch. - `gean/xmss/rust/multisig-glue/src/lib.rs` (same file) — `xmss_verify_aggregated()`, the verifier side. Returns a bool. This is the function every gean node runs on every aggregate it receives. - `gean/xmss/ffi.go` — the CGo bindings: `xmss_aggregate()`, `xmss_verify_aggregated()`, `EnsureProverReady()`, `EnsureVerifierReady()`. The "ensure ready" calls are because the WHIR setup is expensive (allocating large lookup tables) and amortized via a one-time `Once` guard on the Rust side. - `gean/types/block.go` — `AggregatedSignatureProof` is the SSZ-encoded version of the WHIR proof, capped at 1 MiB. Notice the name: it has the word "proof" in it. *This is a cryptographic proof, not a formal-verification proof.* - `gean/types/attestation.go` — `SignedAggregatedAttestation carries an aggregated vote with a zkVM proof`. Same: zkVM proof, not Lean4 proof. When you read gean code, every time you see "proof" it means a SNARK. There is no formal verification in the gean codebase today. ## 17. The intersection: ArkLib Now we connect the two domains. **ArkLib** is Quang Dao's project at CMU. The full name is "Formally Verified Arguments of Knowledge in Lean". It is a Lean4 library that: 1. Defines the abstract notion of an **Interactive Oracle Reduction (IOR)** — a generalized form of interactive proof where the verifier has oracle access to the prover's messages instead of full access. This is the right abstraction for modern SNARKs. 2. Provides **executable specifications** of major SNARK protocols — Sum-Check, Spartan, FRI, BaseFold, FRI-Binius, STIR, **WHIR**, Fiat-Shamir transform. 3. Mechanizes **security proofs** of those protocols (round-by-round knowledge soundness, reductions between security notions). 4. Enables **composition** of protocols via sequential gluing and "virtualization" (mapping inputs/outputs of inner protocols). 5. Is the foundation for future **Rust extraction** so that the verified Lean4 specs can be run as production code. Why this matters for gean: - The aggregation that `multisig-glue` performs is **WHIR**. - WHIR is on ArkLib's roadmap (mentioned in `pq2-08.md` workshop notes from Lean Week Cambridge 2025). - When ArkLib finishes proving WHIR's round-by-round knowledge soundness, that proof transfers — by composition — to gean's signature aggregation. You will not have done any work on gean. ArkLib is the upstream you depend on. - This is the "verify the dependencies, not the application" path (path **(d)** in Part VII). The repo: `https://github.com/Verified-zkEVM/ArkLib`. The umbrella project: `https://verified-zkevm.org/`. --- # Part IV — Lean4, specifically ## 18. What Lean4 is **Lean4** is a programming language and a proof assistant in one. It was created by Leonardo de Moura (formerly Microsoft Research, now AWS) as the successor to Lean 3. The first stable release was in 2023. It is built on **dependent type theory** (a variant of the Calculus of Inductive Constructions, with quotient types and propositional extensionality). The same language is used to: - Define data types and functions (programming). - State theorems (which are types). - Prove theorems (which are programs whose types are theorem statements). - Write tactics and meta-programs (which manipulate other programs). This is the **Curry-Howard correspondence**: propositions are types, proofs are programs. When you "prove a theorem" in Lean4 you are writing a program whose return type is the theorem's statement, and the type checker verifies that the program type-checks. There is no separate proof language. Two consequences of this design: - **Lean4 is a real programming language.** You can write a chess engine in Lean4. You can compile it to native code. People do. - **Proofs and programs share infrastructure.** The same `def` keyword introduces a function and a proof. The same elaborator handles both. Anything you learn about programming in Lean4 transfers to proving, and vice versa. The lead author of the Lean Theorem Prover, Leonardo de Moura, also led the design of Z3 — so Lean4 inherits a lot of pragmatism from the SMT world. ## 19. Dependent types in 30 seconds A dependent type is a type that *depends* on a value. The canonical example is `Vec α n`: the type of vectors of length `n` with elements of type `α`. Two values of `Vec α 3` and `Vec α 4` are different types — you cannot append them without producing a `Vec α 7`, and the type system enforces this. ``` List α : Type Vec α 3 : Type (a vector of length 3) Vec α 4 : Type (a vector of length 4) append : Vec α m → Vec α n → Vec α (m + n) ``` This lets you express things at the type level that ordinary type systems force you to check at runtime. In gean's Go code, `[32]byte` for a hash root is a fixed-size array — the simplest form of dependent typing. Lean4 lets you go arbitrarily further: you can have a type like `BeaconState n` parameterized by the validator count, with functions whose types statically guarantee they preserve `n`. For cryptographic specs, dependent types are essential because the security parameter, the field size, the polynomial degree, the number of rounds, are all statically meaningful. ArkLib uses them everywhere. ## 20. Curry-Howard and why it matters for crypto If propositions are types and proofs are programs, then **a proof of a security property is a Lean4 program**. A statement like "for any prover P that runs in time T, the probability that P fools the verifier is at most ε" becomes a type, and a Lean4 program inhabiting that type is a proof. This means the proofs have all the nice properties of programs: - **They compose.** A proof of WHIR's soundness composes with a proof that XMSS-with-WHIR-aggregation is unforgeable, yielding a proof of unforgeability for the full scheme. - **They are debuggable.** When a proof fails, the elaborator tells you where, just like a compile error. - **They are versionable.** Git diffs of proofs are meaningful. - **They are searchable.** You can `grep` for theorems, ask the elaborator for the type of a sub-expression, navigate to definitions. The downside: proofs are also like programs in being *brittle*. A small change to a definition can break dozens of proofs that depended on the old shape. Maintaining a Lean4 codebase is real engineering, not just math. ## 21. What Mathlib is and why it dominates **Mathlib4** is the community-maintained library of formalized mathematics in Lean4. As of 2025 it contains roughly 1.6 million lines of formal definitions, theorems, and proofs, covering: - Set theory, logic, foundations - Algebra (groups, rings, fields, modules, Galois theory) - Number theory (algebraic, analytic, p-adic) - Topology, measure theory, functional analysis - Algebraic geometry (in progress), category theory - Probability, combinatorics, graph theory - Order theory, lattice theory It is the **single most comprehensive formal math library in any proof assistant**, and it is the main reason Lean4 has the momentum it does. Anything you would want to prove about cryptographic primitives, you can lean on Mathlib4 for the underlying math. Practical implication: when you start Stage 3 of the curriculum (Part VI) and learn Mathlib, you are learning a lot. It has its own conventions, its own naming schemes, its own type-class hierarchy. People spend months becoming fluent. The good news is that you do not need to know all of it — you need to know the slice that touches your work (probably algebra of finite fields, polynomial rings, and probability). ## 22. The Lean4 ecosystem: tools you need to know - **elan** — the toolchain manager (analogous to `rustup`). Installs Lean4 versions and switches between them. - **lake** — the build system (analogous to `cargo`). Manages dependencies, builds projects, runs tests. - **Mathlib4** — the math library. You depend on it via `lake`. - **Lean Server / VS Code extension** — the IDE experience. Lean4 is unusable without an editor that talks to the Lean Server. Use VS Code with the official Lean4 extension. There is also an Emacs mode and an experimental neovim mode. - **Mathlib4's `simp` lemma database** — a vast collection of rewriting rules. The `simp` tactic looks them up. - **`grind`** — a newer tactic for closing arithmetic / boolean goals automatically. Reduces proof effort. - **`omega`** — decision procedure for linear arithmetic over integers and naturals. - **`polyrith`** — closes polynomial-equality goals using Gröbner bases. - **`linarith`** — linear arithmetic over ordered fields. - **doc-gen4** — documentation generator (Mathlib's docs at `leanprover-community.github.io/mathlib4_docs/`). - **Lean Zulip** — `leanprover.zulipchat.com` — the community chat. The single best place to ask "how do I prove X" questions. For our purposes, the libraries that matter most are: - **Mathlib4**: foundation - **ArkLib** (`https://github.com/Verified-zkEVM/ArkLib`): SNARK formalizations - **VCVio**: a Lean library for cryptographic reasoning (oracle queries, computational soundness, etc.) used by ArkLib - **iris-lean**: a port of the Iris program logic (separation logic on steroids) — relevant if you ever do refinement proofs of stateful Go-style code You do not need to install most of these on day one. Just know the names. ## 23. Why Lean4, not Coq A reasonable question. The short answer: it is what the EF picked, and the network effects compound. The longer answer: - **Mathlib4 momentum.** Coq has Mathcomp, Isabelle has the AFP, but Lean4's Mathlib is the only library of formal math that is *growing exponentially* in community contributors as of 2024–2025. - **Modern syntax.** Lean4 is the first proof assistant to genuinely feel like a 21st-century programming language. The syntax is closer to Haskell/Scala than to Coq's Vernacular. This matters for adoption. - **Tactic framework.** Lean4 lets you write tactics in Lean4 itself, which means the tactic ecosystem grows quickly. - **Industrial backers.** AWS hired de Moura. Nethermind funds Lean-EVM. The EF funds the snarkification track. There is real money behind Lean4 right now. - **It is what ArkLib is in.** Quang Dao's ArkLib is Lean4. Switching to Coq would mean rewriting it. - **Lean-EVM is in Lean4.** Nethermind's verified EVM model is in Lean4. End-to-end EVM verification work uses Lean4. Coq is not worse on technical merits — CompCert (the verified C compiler) is Coq, and is one of the most successful FV projects ever. But the *consensus client* and *cryptography* corners of the EF ecosystem have already standardized on Lean4, and you should follow that gravity. --- # Part V — Prerequisites: what to learn *before* opening Lean4 This is the "you cannot skip this" section. People who open *Theorem Proving in Lean 4* without these prerequisites bounce off. People who have these prerequisites find Lean4 hard but tractable. The prerequisites split into three buckets: **mathematics**, **computer science**, and **cryptography**. None of them require Lean4. All of them can be done with paper, pen, and existing textbooks. ## 24. Mathematics floor You need to be comfortable with the following at the *I can read the symbols and follow a proof* level — not the *I can produce original research* level. **Logic**: - Propositional logic: `∧`, `∨`, `¬`, `→`, `↔`, truth tables, normal forms. - First-order logic: `∀`, `∃`, quantifier scope, prenex form. - Natural deduction style proofs: introduction and elimination rules, especially `→` and `∀`. - Induction (over naturals, lists, trees) and strong induction. - The difference between *classical* and *constructive* logic. Lean4 is constructive by default but admits classical reasoning via `Classical.em`. You will need to know which mode you are in. **Set theory and functions**: - Sets, subsets, unions, intersections, set-builder notation. - Functions, domain, codomain, image, preimage, injectivity, surjectivity, bijection. - Equivalence relations, equivalence classes, quotients. - Cartesian products, n-tuples. - Cardinality (countable / uncountable, but only at a basic level). **Abstract algebra**: - Groups, rings, fields, modules. - Homomorphisms and isomorphisms. - Ideals (basic level). - **Finite fields** specifically — every cryptographic SNARK works over a finite field. You will see `KoalaBear` everywhere; it is a 31-bit prime field. - Polynomial rings `F[X]`, polynomial evaluation, factorization, roots. - Multivariate polynomials (at a basic level — you will need them for Sum-Check). **Probability**: - Basic discrete probability: events, conditional probability, independence, expectation. - Random variables and distributions. - Concentration (Markov, Chebyshev, Chernoff at hand-wave level). - **Why you need this**: cryptographic soundness is a probabilistic statement ("a cheating prover succeeds with probability at most ε"). Soundness proofs are probability arguments. **Coding theory** (only if you want to read ArkLib in detail): - Reed-Solomon codes, distance, list decoding. - Proximity gaps, Johnson bound. - These are advanced. Skip them on the first pass and circle back when you read FRI / WHIR papers. ## 25. Computer science floor **Functional programming**: - Immutability and pure functions. - Pattern matching on algebraic data types. - Recursion on lists and trees. - Higher-order functions: `map`, `filter`, `fold`. - Algebraic data types (tagged unions / sum types). - Type classes / traits / interfaces (if you've used Rust or Scala, you're set). If you have written Rust at any reasonable depth, you have all the functional programming you need. If you have only written Go, you should spend a few days on Haskell or OCaml first — the mental adjustment to *immutable everything* is harder than learning Lean4 syntax. **Type theory**: - Simply typed lambda calculus (one afternoon's reading). - Polymorphism (`forall a. List a -> Int`). - Just enough about dependent types to read `Vec α n` without panicking. - The Curry-Howard correspondence at the level of "propositions are types". You do *not* need to study type theory deeply. You need to recognize the words. **Program semantics**: - Operational semantics (small-step, big-step) — what it means to "execute" a program in the abstract. - State machines and transition systems. - Hoare logic (Part II §7). - Loop invariants. The textbook for all of this is **Pierce's *Software Foundations*, Volume 1: *Logical Foundations***. It is written in Coq, not Lean4, but the concepts transfer 1:1. You can do the reading and skip the Coq exercises. ## 26. Cryptography floor This is for understanding ArkLib and the SNARK side. You can do most of the consensus FV work without it. **Hash functions and Merkle trees**: - Collision resistance, preimage resistance, second-preimage resistance. - Random oracle model (informally). - Merkle trees, Merkle proofs, batch openings. - Hash-based signatures: Lamport, Winternitz, **XMSS**. **Interactive proofs**: - Σ-protocols (Schnorr is the canonical example). - Completeness, soundness, zero-knowledge. - The Fiat-Shamir transform. - Knowledge soundness vs argument soundness. - Round-by-round knowledge soundness (the property ArkLib proves). **Polynomial protocols** (at hand-wave level for Stage 1; deep for Stage 5): - **Sum-Check protocol**: the workhorse of modern SNARKs. Proves that a polynomial sums to a known value over the boolean hypercube. - **Polynomial commitment schemes**: commit to a polynomial, later open it at a point, prover proves the opening is consistent. - **FRI**: a polynomial commitment scheme based on Reed-Solomon codes and recursive folding. - **WHIR**: the post-quantum SNARK gean uses. Stands for "Weights of Hashes for Improved Recursion" (or similar — the meaning of the acronym is less important than knowing it is a Reed-Solomon-based STARK / SNARK that improves on FRI in several dimensions). - **BaseFold**, **STIR**, **FRI-Binius**: variants and successors. Same family. You do not need to *understand* these protocols deeply on day one. You need to recognize the names and know that they all do roughly the same thing (prove that a committed polynomial has some property without sending the polynomial itself). ## 27. Concrete pre-Lean4 reading list Ordered by how directly they support what you will be doing. None of these are required cover-to-cover. 1. **Velleman, *How to Prove It* (3rd ed)**. The proof-technique foundation. If you have never written a ε-δ proof or a strong induction proof, start here. Skim if you have. Skip if you have a math degree. 2. **Pierce et al., *Software Foundations Vol 1: Logical Foundations*** — `https://softwarefoundations.cis.upenn.edu/lf-current/index.html`. Free online. Coq-based but transferable. Read chapters 1–8 (Basics through Maps). The Hoare logic chapters in Vol 2 are also worth skimming. 3. **Boneh & Shoup, *A Graduate Course in Applied Cryptography***. Free PDF at `https://toc.cryptobook.us/`. Read chapter 19 (interactive proofs and zero-knowledge) for the SNARK foundation. Optionally chapters 14–15 for hash-based signatures. 4. **Justin Thaler, *Proofs, Arguments, and Zero-Knowledge***. Free PDF at `https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.html`. The canonical SNARK textbook. You want chapters 1–4 (interactive proofs, sum-check, IPs vs IOPs) and chapters 8–10 (FRI, polynomial commitments). Heavy but worth it. 5. **The leanSpec source code** (`/Users/bankat/Documents/protocol/gean-agent/leanSpec/src/lean_spec/subspecs/chain/`). Read the Python reference spec for state transition and fork choice. This is what you would be modeling in Lean4 if you took the spec-first approach. Reading it tells you the *shape* of the spec you would need to write. 6. **gean source code, the FV-target files**: - `gean/statetransition/justifiable.go` (33 lines, the smallest target) - `gean/statetransition/block.go` (block header invariants) - `gean/statetransition/attestations.go` (vote application) - `gean/forkchoice/spec.go` (the spec oracle for LMD GHOST) - `gean/forkchoice/protoarray.go` (the production tree) Read these *as if you were going to write a Lean4 spec of them*. Annotate the invariants. Identify the preconditions. This is the most useful thing you can do before opening Lean4. 7. **The Lean Week Cambridge 2025 workshop notes** at `pm/workshops-and-interops/2025/lean-week-cambridge/`. Read at minimum: - `pq1-07.md` — Hicks on the verified zkEVM project (3-track structure, 2027 timeline) - `pq1-08.md` — Dao on ArkLib intro - `pq2-05.md` — Sutherland on end-to-end FV and Lean-EVM - `pq2-08.md` — Dao on ArkLib walkthrough (more concrete) - `index.md` — the speaker map; identify the people you should follow This list is enough for several weeks of work. Do *not* try to do it all in one sitting — read in parallel with starting Lean4 itself, not before. ## 28. Gean-specific orientation Before you can write a Lean4 spec of any gean component, you have to know what the component does at the level of every line. Specifically: - `statetransition/justifiable.go`: 33 lines. Three rules: distance ≤5, perfect square, pronic number. *Number-theoretic.* You will need facts from `Mathlib.Data.Nat.Sqrt` and possibly `Mathlib.Data.Nat.Squarefree`. The Lean4 spec is roughly: define `IsJustifiable : ℕ → ℕ → Prop`, define a corresponding `decide` function, prove they agree, prove a few sanity properties (transitivity-like). - `forkchoice/spec.go`: 119 lines. `SpecComputeBlockWeights`, `SpecComputeLMDGhostHead`. *Graph-theoretic.* Walking parent chains, computing weights, picking heaviest child with lexicographic tiebreaker. Will need `Mathlib.Data.List`, `Mathlib.Data.Finset`. The Lean4 spec is a function over a finite map of blocks; properties to prove are termination (the parent walk reaches the start slot), determinism, and consistency with the proto-array implementation. - `forkchoice/protoarray.go`: more complex, adversarial. The proto-array is a tree with parent pointers, scores, and a root. Invariants: no cycles, every node's score equals the sum of votes for its subtree, the head returned by `FindHead` is always a leaf (or the root) of the subtree rooted at the justified root. *Save this for later.* - `xmss/rust/multisig-glue/src/lib.rs`: out of scope for direct verification. Read it once to understand the WHIR API surface. The verification of WHIR itself happens upstream in ArkLib. When you read these files, take notes on **invariants** (not implementations). An invariant is a sentence of the form "at every point, X is true". Examples: - "at every point, if a block has a parent, the parent is in the proto-array tree" - "at every point, the score of a node equals the sum of scores of its descendants plus its own attestation weight" - "for any slot s and finalized slot f, `SlotIsJustifiableAfter(s, f)` returns true if and only if `s > f` and `s - f` is in the set `{1,2,3,4,5} ∪ squares ∪ pronics`" Those sentences are the things you would prove in Lean4. Writing them down in plain English, before any Lean4, is 80% of the work. --- # Part VI — Learning Lean4: a phased curriculum A **5-stage roadmap**. Each stage has a goal, a primary resource, a deliverable, and explicit non-goals. There are no timelines — the goal is sequencing, not scheduling. ## Stage 0 — Setup **Goal**: have a working Lean4 environment so that nothing blocks you when you start Stage 1. **Steps**: 1. Install **elan** (the toolchain manager). Single shell command from `https://lean-lang.org/`. 2. Use elan to install the latest stable Lean4 toolchain. 3. Install **VS Code** + the official **Lean4 extension** (`leanprover.lean4`). 4. Create an empty Lake project (`lake new my_first_lean_project`) and verify it builds. 5. Add Mathlib4 as a dependency (one line in `lakefile.lean`). The first build downloads ~5 GB of cached `.olean` files. Have it run while you do something else. 6. Open the project in VS Code, type `import Mathlib`, wait for the elaborator to come online (the orange bar in the status line). When the bar disappears and you can hover over Mathlib identifiers and see types, Stage 0 is done. **Deliverable**: a screenshot of your VS Code with `import Mathlib` working. **Non-goals**: do not try to write any proofs yet. Do not try to understand `lakefile.lean`. Do not customize anything. ## Stage 1 — Functional Lean **Goal**: become fluent in Lean4 *as a programming language*, separately from Lean4 as a proof assistant. You should be able to read and write data types, pattern matches, recursive functions, type classes, and the do-notation for monads. **Primary resource**: **David Christiansen, *Functional Programming in Lean*** — `https://lean-lang.org/functional_programming_in_lean/`. **What to read**: chapters 1 through 5 (Hello World through Type Classes). Skip the IO chapters on the first pass — you do not need them yet. **Deliverable**: rewrite **one small piece of gean code** as a pure Lean4 function. Recommended target: the `SlotIsJustifiableAfter` function from `gean/statetransition/justifiable.go`. It is 33 lines, takes two `uint64`s, returns a `Bool`. Translate it to Lean4 as a function `slotIsJustifiableAfter : Nat → Nat → Bool`. Do not prove anything about it yet. Just get it to compile and test it on a few inputs (`#eval slotIsJustifiableAfter 10 5`). **Non-goals**: - Do not prove anything in this stage. - Do not use Mathlib's `Nat.sqrt` yet — write your own naive square-root if needed. - Do not worry about `Float` precision (the Go code uses `math.Sqrt`; you can use integer arithmetic). - Do not try to understand `do` notation, monads, or `IO` deeply. Skim the chapters and move on. ## Stage 2 — Theorem Proving **Goal**: be able to *state* and *prove* simple theorems in Lean4 using tactics. You should be comfortable with `intro`, `apply`, `exact`, `rw`, `simp`, `induction`, `cases`, `exists`, `constructor`, and the basic equality reasoning. **Primary resource**: **Avigad, de Moura, Kong, *Theorem Proving in Lean 4*** — `https://lean-lang.org/theorem_proving_in_lean4/`. The canonical book on Lean4 as a proof assistant. **What to read**: chapters 1 through 7 (Introduction through Inductive Types) and chapter 5 specifically on Tactics. The chapters on the axiom of choice and quotients can wait. **Deliverable**: prove **one property** of your `slotIsJustifiableAfter` function from Stage 1. Suggested theorem: > *For all naturals s and f, if `s > f` and `s - f ≤ 5`, then `slotIsJustifiableAfter s f = true`.* This is the easiest of the three rules to prove, because there is no number theory in it. It teaches you the basic rhythm: `intro` the variables and the hypothesis, `unfold` the definition, `simp` away the trivial parts, and close the goal with `rfl` or `decide` or `omega`. **Non-goals**: - Do not try to prove the perfect-square or pronic-number rules yet — those need Mathlib lemmas about square roots, which you will learn in Stage 3. - Do not try to handle the `Float` precision question (i.e., don't try to prove that the `math.Sqrt`-based Go implementation matches your Lean4 integer-only spec). That is a refinement question for much later. - Do not learn `term mode` vs `tactic mode` formally. Use whichever the book uses for each example. ## Stage 3 — Mathlib fluency **Goal**: learn to *find and use* lemmas from Mathlib4. This is where most beginners get stuck, because Mathlib has its own naming conventions, its own type-class hierarchy, and its own way of doing things. Becoming productive with Mathlib is the threshold between "Lean4 hobbyist" and "Lean4 contributor". **Primary resource**: **Avigad, Massot, *Mathematics in Lean*** — `https://leanprover-community.github.io/mathematics_in_lean/`. The canonical book on writing math with Mathlib. **What to read**: the whole book is good, but if you must triage: chapters 1–4 (Introduction through Sets and Functions), chapter 5 (Elementary Number Theory), and the chapter on basic algebraic structures. Skip the topology and analysis chapters unless you find them interesting. **Deliverable**: **finish proving the perfect-square rule** of `slotIsJustifiableAfter`. The theorem is: > *For all naturals s and f, if `s > f` and `s - f` is a perfect square, then `slotIsJustifiableAfter s f = true`.* This requires you to find the right lemma in `Mathlib.Data.Nat.Sqrt` (the module about integer square roots), use it to prove that your spec matches, and discharge the obligation. The Mathlib lemma you want is probably `Nat.sqrt_eq_iff_sq_eq` or similar — *finding* it is the exercise, not just *using* it. **Non-goals**: - Do not try to prove the pronic-number rule yet. It is harder because the characterization involves the discriminant (`4*delta + 1` is an odd perfect square). - Do not try to *contribute* to Mathlib. Reading and using is enough. - Do not learn the entire Mathlib type-class hierarchy. Look up class names as needed. ## Stage 4 — Domain specialization: consensus **Goal**: write a Lean4 spec of one isolated gean component, prove a non-trivial invariant, and *write up* what you did in plain English so your team can read it. This is where you start producing real value for the project. **No primary book**: you are now beyond textbooks. Your resources are: - Mathlib4 source (`https://github.com/leanprover-community/mathlib4`) - Mathlib4 docs (`https://leanprover-community.github.io/mathlib4_docs/`) - The Lean Zulip (for asking questions) - The gean source code **Recommended target**: **`gean/statetransition/justifiable.go`**. The full module. Three rules. You have already proved one or two by Stage 3. Now finish the third (pronic numbers) and prove a higher-level theorem like: > *For any state S, if S is `IsJustifiable` after finalized slot f, and all the rules say so, then the conjunction of the three rules characterizes exactly the set of justifiable slots.* In other words: prove that the *Go function* is correct *with respect to your formal definition* of justifiability. This is the smallest possible end-to-end formal verification of a gean component. It is also the smallest possible *useful* formal verification. The proof is not deep, but the *practice* of producing it teaches you everything: how to write a spec, how to break the proof into lemmas, how to organize the file, how to review it, how to share it. **Deliverable**: a Lean4 file containing your spec + proofs, plus a 1–2 page Markdown writeup of "what I proved, what I trusted, and what is still unverified". **Non-goals**: - Do not try to verify `forkchoice/protoarray.go` in this stage — it is much more complex (graph invariants, mutable state). - Do not try to integrate the Lean4 code with gean's Go code. Keep them separate. The Lean4 work is documentation, not deployment. - Do not try to bridge to the leanSpec Python reference. That is a separate thread. ## Stage 5 — Domain specialization: cryptography (ArkLib) **Goal**: be able to *read* ArkLib's code, understand what has been proved, and explain it to your team. You are not necessarily writing new ArkLib code — you are becoming the gean team's interpreter for the upstream FV work. **Resources**: - ArkLib repo: `https://github.com/Verified-zkEVM/ArkLib` - Quang Dao's workshop talks: `pm/workshops-and-interops/2025/lean-week-cambridge/pq1-08.md`, `pq2-08.md` - Justin Thaler's textbook (you read it in Part V) - The WHIR paper (search "WHIR Reed-Solomon proximity STIR") **Deliverable**: a writeup that answers, in plain English: *"What has ArkLib proved about WHIR? What does it mean for the soundness of gean's signature aggregation? What is the gap between an ArkLib WHIR proof and a guarantee about gean's `xmss_verify_aggregated` function?"* This is **liaison work**, not original research. You are translating between two communities (ArkLib developers and gean developers) so that the gean team knows what to wait for and what to ignore. **Non-goals**: - Do not try to write your own SNARK. You will not finish. - Do not try to formalize a new protocol from scratch. - Do not try to extract ArkLib's Lean4 code to Rust to plug into gean. The extraction tooling is not ready. ## A note on stage transitions You will notice I have not given you time estimates. That is deliberate: people learn at very different speeds, and there is no benefit to telling yourself "Stage 2 should take two weeks" when in fact it takes you four. The right signal that you are ready to move from Stage N to Stage N+1 is the **deliverable**: if you have produced the deliverable and you understand *what you did*, you are ready. If the deliverable feels uncertain, redo Stage N until it does not. The other signal is **ergonomic comfort**: if you are still spending most of your Lean4 time fighting the tools (the elaborator hangs, you cannot find lemmas, error messages confuse you), you are not ready to move on. Lean4 fluency is a real prerequisite for Lean4 productivity, and the curriculum is designed so that each stage increases ergonomic comfort. --- # Part VII — How Lean4 will (and will *not*) integrate with gean This is the section that resolves the question in the original prompt: *how will Lean4 be applicable in our Go codebase seamlessly, which areas will need it.* The honest answer is **not seamlessly**. There is no `import "lean4"` in your Go files. Anyone who tells you otherwise has confused Lean4 with the lean Ethereum *spec*. But there are four real integration paths, each with different trade-offs. We discuss them in order of "how seamless" they are not. ## 29. The four integration paths ### Path (a): Spec-first verification **The idea**: Port `leanSpec` (currently Python) to Lean4 module by module. Treat the Lean4 spec as the source of truth. Prove safety and liveness theorems against the Lean4 spec. Generate spec test fixtures from it (the same way leanSpec generates them today). Treat gean as one implementation that must conformance-test against the fixtures. **What you need**: - A complete Lean4 model of the protocol — types, state, transition functions. - Theorem statements for the safety (no two finalized blocks at the same slot) and liveness (eventual finality under honest majority) properties. - Proofs of those theorems against the Lean4 spec. - A test fixture generator that runs the Lean4 spec and emits SSZ-encoded JSON (Lean4 can compile to native code, so this is doable). - Conformance tests on every implementation — gean already has these, they would just point at Lean4-generated fixtures instead of Python-generated ones. **Pros**: Highest leverage. One verified spec, many clients benefit. Aligns with the EF's 2027 target. **Cons**: Longest road. Porting leanSpec is real work. Mathlib does not have all the Pydantic / SSZ machinery you need; you would build it. **Recommendation**: This is a *team* project, not an individual one. Watch for it to start at the EF level. Do not start it yourself. ### Path (b): Algorithm-level verification **The idea**: Pick **one** algorithm from gean. Write it in Lean4. Prove its invariants. Transcribe back to Go by hand. Use the Lean4 file as living documentation. **What you need**: - A Lean4 spec of one algorithm (e.g., `SlotIsJustifiableAfter` from Stage 4 of the curriculum, or eventually `protoarray`). - A proof of the invariants you care about. - A clear correspondence between the Lean4 file and the Go file. **Pros**: Doable by one person. No FFI, no extraction, no toolchain integration. Produces real value (the proof catches real bugs and is real documentation). **Cons**: The Lean4 file and the Go file can drift. You need a process for keeping them in sync (probably a CI check that the Go function and the Lean4 function agree on a corpus of test inputs). **Recommendation**: **Start here.** This is the right path for a single contributor in 2026. ### Path (c): Verified extraction **The idea**: Write the algorithm in Lean4, prove its properties, then *extract* the Lean4 code to a target language (C, Rust), and link the extracted code into gean via FFI — exactly the same way you already link `xmss/rust` libraries into Go. **What you need**: - Lean4 has a built-in compiler that produces native code. It can also be configured to emit C. - A Lean4-to-Rust extraction toolchain. **This does not exist in production-ready form yet** — there are research projects but none are ready for a production consensus client. - A way to link the extracted code into gean. **Pros**: Most "seamless" of the four. The proved-correct code actually runs in production. No drift between spec and implementation. **Cons**: The extraction tooling is not there. You would be doing research, not engineering. **Recommendation**: **Wait.** Track Sébastien Gouëzel's and Jean-François Monin's extraction work. Watch for ArkLib's extraction announcements (Quang Dao mentioned them as a near-term goal). Revisit in 2026 or 2027. ### Path (d): Cryptographic dependency verification **The idea**: Don't verify gean. Verify the things gean depends on. Specifically: contribute to ArkLib's formalization of WHIR (the SNARK that `multisig-glue` uses), and to a future Lean-XMSS (the underlying signature scheme). **What you need**: - Stage 5 of the curriculum: ability to read ArkLib. - Familiarity with the WHIR paper. - Willingness to contribute upstream rather than to gean directly. **Pros**: Massive leverage. One ArkLib proof of WHIR transfers to *every* SNARK system that uses WHIR — gean, ream, zeam, ethlambda, qlean, lantern, and any future client. This is where the EF money already is. **Cons**: You are working in someone else's repo, on someone else's schedule. The work does not directly improve gean's codebase — only its trust base. **Recommendation**: **Combine with path (b).** Spend half your time on (b) (algorithm-level proofs of consensus components) and half on (d) (reading and tracking ArkLib's WHIR work). The combination gives you both depth (you are doing real proofs in path b) and breadth (you are learning the upstream world in path d). ## 30. Recommendation, in one paragraph Start with **path (b)**: pick `gean/statetransition/justifiable.go` as your first target, because it is the smallest, most isolated, most number-theoretic file in the codebase, and it is *exactly* the kind of thing where formal verification has obvious value (you cannot test number-theoretic properties on `uint64` exhaustively, and the float-precision question is real). When you finish that, move to one piece of `forkchoice/spec.go`. In parallel, follow **path (d)**: read ArkLib commits weekly and write 1-paragraph summaries for the team. Skip path (a) until the EF starts it. Skip path (c) until the extraction tooling matures. --- # Part VIII — Where Lean4 specifically helps gean Concrete files. Concrete reasons. Use this as a map when you are looking for "what should I formalize next". ## 31. Tier 1 — Highest priority (start here) These are isolated, mathematical, and would benefit immediately from Lean4 verification. ### `gean/statetransition/justifiable.go` - **Why it's a great target**: 33 lines. Pure function. Three mathematical rules: distance ≤5, perfect square, or pronic number. Zero dependencies on other parts of the codebase. Number-theoretic — exactly the kind of thing where exhaustive testing fails and a proof catches the edge cases. - **What to prove**: that `SlotIsJustifiableAfter(s, f) = true` if and only if `s > f` and `s - f ∈ {1,2,3,4,5} ∪ {n² : n ∈ ℕ} ∪ {n(n+1) : n ∈ ℕ}`. - **Latent bug to look for**: the function uses `math.Sqrt(float64(delta))` to compute integer square roots. For `delta` close to `2^53`, the `float64` representation loses precision and the cast back to `uint64` can be off by one. Either the function handles this correctly (in which case the proof is satisfying), or it doesn't (in which case the proof finds a real bug). Either outcome is valuable. - **Lean4 effort**: small. A couple of hundred lines including the spec, the function, and the proofs. - **Mathlib needed**: `Mathlib.Data.Nat.Sqrt`, basic algebra of squares. ### `gean/statetransition/block.go` (block header invariants only) - **Why**: Block header validation is the boundary check that lets the rest of the state transition proceed. It enforces `block.Slot > parentHeader.Slot`, the proposer index condition, the parent root condition, and the finalization-boundary check. - **What to prove**: write down the six or seven preconditions as a Lean4 predicate. Prove that if the predicate holds, `ProcessBlockHeader` produces a state with the new header installed. Prove that the predicate is necessary (i.e., if any precondition fails, the function rejects). - **Latent bug to look for**: the historical-block-hashes overflow guard (limit 262,144) is the kind of off-by-one that bites you ten years into mainnet. A Lean4 proof of "the bitlist is well-formed at every point" would be valuable. - **Lean4 effort**: medium. You need to model `BeaconState` and `BlockHeader` as Lean4 records. - **Mathlib needed**: very little; this is mostly straightforward state-machine reasoning. ### `gean/forkchoice/spec.go` (the LMD GHOST oracle) - **Why**: This file is *already* a spec — its comment literally says it is "the spec-compliant LMD GHOST implementation for testing, used as a debug oracle to validate proto-array produces identical results". That makes it the natural target for a Lean4 spec, because the gean code is already written in the simplest possible style. - **What to prove**: termination of the parent-walking loop in `SpecComputeBlockWeights` (it terminates because it cannot revisit a block above `startSlot`), determinism of `SpecComputeLMDGhostHead` (the lexicographic tiebreaker in `rootGreaterThan` is total), and equivalence with the proto-array implementation. - **Lean4 effort**: medium. Termination of a loop over a finite tree is a standard well-foundedness argument. - **Mathlib needed**: `Mathlib.Data.Finset`, well-founded recursion. ## 32. Tier 2 — High priority (after Tier 1 is comfortable) ### `gean/forkchoice/protoarray.go` - **Why**: This is the production fork choice. Bugs here split the chain. - **What to prove**: tree invariants (no cycles, every node has a parent in the tree, scores are consistent with the children), `FindHead` always returns a node in the subtree of the input root, `Prune` does not remove nodes above the finalized root. - **Latent bug surface**: the proto-array is a *mutable, indexed, in-place* data structure. Mutable state is harder to verify than pure functions. You will need to model the proto-array as a sequence of states with transitions. - **Lean4 effort**: large. This is the kind of thing where you start with one tiny invariant (e.g., "every parent index points to a valid node") and expand outward. ### `gean/statetransition/attestations.go` - **Why**: Vote application is the safety-critical path for finality. A bug here that double-counts votes or mis-attributes them to the wrong validator can break finality. - **What to prove**: each attestation increments exactly one vote per validator, no double-counting, justification thresholds are computed correctly. - **Lean4 effort**: medium-large. Depends on how much of `BeaconState` you have already modeled. ### `gean/forkchoice/votes.go` - **Why**: The vote-delta computation is the bridge between attestations and the proto-array. Errors here propagate everywhere. - **What to prove**: the delta computed from a batch of new attestations is exactly the difference between the new and old vote counts. (No off-by-one, no missing validator.) - **Lean4 effort**: small-medium. ## 33. Tier 3 — Out of scope (for now) ### `gean/p2p/`, `gean/storage/`, `gean/api/`, `gean/cmd/` - **Why out of scope**: networking, persistent storage, HTTP API, and CLI plumbing are *reliability* concerns, not *safety* concerns in the formal sense. They have lots of bugs but those bugs are caught by integration testing. There is nothing in their behavior that would benefit from Lean4 — the properties you would want to prove (e.g., "the GossipSub subscription is correctly maintained") are not the kinds of things that have clean mathematical statements. - **Exception**: SSZ encoding (`gean/types/`) could in principle be formally verified for round-tripping. There is academic precedent (Project Everest verifies TLS message encoding). But it is a large effort for limited safety value compared to the consensus targets above. ### `gean/xmss/rust/multisig-glue/` (WHIR aggregation) - **Why out of scope for *direct* gean verification**: the FV target is the WHIR protocol itself, not gean's wrapper of it. ArkLib is doing this work upstream. Your job (as gean's Lean4 person) is to *track* it, not to redo it. - **What to do instead**: read ArkLib's WHIR formalization as part of Stage 5 of the curriculum. Write a writeup explaining what ArkLib has proved and what gap (if any) remains for gean's specific use of WHIR. ## 34. The honest reckoning Looking at the gean codebase as a whole, the realistic FV-shaped surface is small: - ~33 lines in `justifiable.go` - ~120 lines in `forkchoice/spec.go` - ~100 lines in `statetransition/block.go` (the validation predicates) - ~280 lines in `statetransition/attestations.go` - ~180 lines in `forkchoice/protoarray.go` Total: ~700 lines of gean code worth formally verifying. The other ~10,000 lines are networking, storage, plumbing, types, and tests — none of which need or benefit from Lean4. **The signal-to-noise ratio of formal verification in a consensus client is much better than people expect.** You are not trying to verify the whole codebase. You are trying to verify the small core that, if it has a bug, breaks the chain. This is good news. 700 lines is *tractable*. One person, working consistently, with the right Lean4 fluency, can verify it. That is the realistic target for "gean has a Lean4 component" by 2027. --- # Part IX — Becoming the team's Lean4 person The original prompt asks how to "be a Lean4 expert for my team". Reframe this. The word "expert" implies a finished state, and Lean4 is too young and the field is moving too fast for that to mean anything. The realistic role is **Lean4 liaison**: the person on the gean team who can read ArkLib commits, attend the snarkification calls, translate what is happening into action items, and produce the gean-specific Lean4 work that other teams will not do for you. In a community of ~50 people doing this work worldwide, *anyone* fluent in Mathlib + ArkLib's IOR style is in the top decile. The bar is lower than you think. You do not need to be Quang Dao. You need to be someone Quang Dao can have a productive conversation with. ## 35. The four habits of a Lean4 liaison These are the weekly habits that, sustained, produce the role. ### Habit 1: Read one ArkLib PR per week ArkLib has a steady stream of pull requests. Subscribe to the repo (`https://github.com/Verified-zkEVM/ArkLib`), pick one PR per week, read it, and write a one-paragraph summary in your team channel. The summary answers: *what was added, what protocol or property does it concern, why does it matter for lean Ethereum's signature aggregation*. The act of writing the summary is what produces the learning. After a few months you will know the IOR framework intimately, you will have a feel for ArkLib's coding conventions, and you will be able to read ArkLib code as fluently as you read Go. ### Habit 2: Track Lean-EVM monthly Nethermind's Lean-EVM is the other major Lean4 effort in the lean Ethereum world. It is more relevant to execution than to consensus, but it is the closest existing example of "a real consensus-adjacent client component formalized in Lean4". Skim the commit log monthly. Take notes on which parts of the EVM they have proved and which are still TODO. ### Habit 3: Maintain a "verified facts about gean" file Create a Lean4 file in your gean repo (or a sibling repo) called `verified_facts.lean`. Every month, add one new theorem about gean. Start tiny: prove that `SlotIsJustifiableAfter(s, f)` is `false` when `s ≤ f`. Then prove the perfect-square rule. Then the pronic-number rule. Then move to `forkchoice/spec.go`. The file does not have to be deployed. It does not have to be linked to gean's Go code. It is *documentation in the form of theorems*. Each new theorem teaches you something, and the file accumulates value over time. ### Habit 4: Attend the EF snarkification calls and Lean Together The Ethereum Foundation runs a regular snarkification call (cadence varies — check with Alex Hicks). The Lean community runs an annual conference called Lean Together. Both are where you meet the people doing this work. You do not have to talk; just listen. The contextual knowledge of *who is working on what* is irreplaceable. ## 36. The people to follow From the speaker list at `pm/workshops-and-interops/2025/lean-week-cambridge/index.md` and from the broader Lean4 community: **Lean Ethereum FV specifically**: - **Quang Dao** (CMU) — ArkLib lead, the single most relevant person for SNARK formalization in Lean4. Twitter: `@QuangVDao`. - **Alex Hicks** (EF — snarkification) — runs the verified zkEVM project, the umbrella for this work. Twitter: `@alexanderlhicks`. - **Julian Sutherland** (Nethermind) — Lean-EVM lead, end-to-end formal verification. Workshop notes credit him with the 99.99%-passing Lean-EVM model. - **Banri Yanahama** (Nyx Foundation) — listed under PQ formal verification at Lean Week. - **Katy Hristova**, **Ilia Vlasov** (Nethermind) — also on the FV track. **Lean4 / Mathlib core community**: - **Leonardo de Moura** — Lean4 author. Now at AWS. - **Patrick Massot** — Mathlib coordinator, co-author of *Mathematics in Lean*. - **Sébastien Gouëzel** — Mathlib heavyweight, prolific contributor. - **Heather Macbeth** — Mathlib analysis lead. - **Mario Carneiro** — Mathlib infrastructure, decision procedures. - **Kim Morrison** — Mathlib category theory and infrastructure. You do not need to follow all of these. You need to recognize the names when they appear in commits or in workshop notes. ## 37. Communities - **Lean Zulip**: `leanprover.zulipchat.com`. Free to join. Active. The single best place to ask "how do I prove X" questions. Channels to subscribe to: `#new members`, `#general`, `#mathlib4`, `#mathlib4 > Mathlib`, and (eventually) any channel related to ArkLib. - **Verified zkEVM**: discussions happen partly in the ArkLib repo issues, partly in the EF snarkification channels. - **Lean Together**: annual conference. Recordings on YouTube. Watch the keynotes. - **leanprover-community.github.io**: the community hub. Has the learning portal, the docs, and the package directory. ## 38. The unwritten rules A few cultural notes that the textbooks do not mention but that matter when you join the Lean Zulip: - **Ask questions in `#new members`, not `#general`.** The community is welcoming but the channels are organized. - **Show your code.** When you ask a question, paste a minimal failing example. People will fix it for you in minutes if they can copy-paste it; they will ignore you if they have to guess. - **Search the Zulip archive first.** Most beginner questions have been asked. The search is good. - **Use `#mwe`** ("minimal working example") in your titles. It is the convention. - **Mathlib contributions are expected to be small and well-named.** A first PR that renames a lemma to fit the convention is welcome. A first PR that adds 500 lines of new theory is not. - **Be patient with the build times.** Mathlib is huge. A clean build takes hours. Use the cached `.olean` files (Mathlib's cache mechanism) to avoid rebuilding from scratch. --- # Part X — Quick reference: glossary, links, action checklist ## 39. Glossary Terms used in this document, alphabetically, with one-sentence definitions. Refer back to this when you encounter a word in a workshop note. - **3SF-mini**: the simplified three-slot finality protocol used in Lean Ethereum devnets, with justification rules involving perfect squares and pronic numbers (see `gean/statetransition/justifiable.go`). - **Argument of knowledge (ARK)**: an interactive cryptographic protocol where the prover convinces a polynomially bounded verifier that they know a witness, with computational soundness. - **ArkLib**: Quang Dao's Lean4 library of formally verified SNARK protocols. Repo: `https://github.com/Verified-zkEVM/ArkLib`. - **BaseFold**: a polynomial commitment scheme based on Reed-Solomon codes, similar to but distinct from FRI and WHIR. Used by some STARK systems. - **BCS**: a generic transformation from interactive oracle proofs to non-interactive arguments via Fiat-Shamir; named after Ben-Sasson, Chiesa, Spooner. - **Curry-Howard correspondence**: the equivalence between propositions and types, and between proofs and programs. Foundation of dependent type theory. - **Dependent type**: a type that depends on a value (e.g., `Vec α n`). Lean4 has them; Go does not. - **EDSL**: embedded domain-specific language. A DSL implemented as a library inside a host language. - **Elaborator**: the part of Lean4 that turns surface syntax into kernel-level terms. Sophisticated; handles type inference, type-class resolution, unification. - **Fiat-Shamir transform**: the universal procedure for turning an interactive proof into a non-interactive one by replacing verifier randomness with hashes of the transcript. - **FRI**: Fast Reed-Solomon Interactive Oracle Proof of Proximity. A polynomial commitment scheme used by ethSTARK and others. - **Gean**: this client. A Go-based consensus client for Lean Ethereum. `https://github.com/geanlabs/gean`. - **Hoare logic**: the formal system for reasoning about imperative programs using preconditions, postconditions, and loop invariants. - **IOR**: Interactive Oracle Reduction. A generalized form of interactive proof used by ArkLib as the abstraction for SNARK protocols. - **Justification (consensus)**: the process by which a slot becomes a candidate for finalization. In 3SF-mini, governed by the rules in `justifiable.go`. - **Kernel (proof assistant)**: the small, audited type checker that is the trusted computing base of Lean4. A few thousand lines. - **KoalaBear**: the 31-bit prime field used by leanMultisig. Chosen for hardware-friendly arithmetic. - **Lake**: Lean4's build system, analogous to Cargo. - **LCIR**: Lean Compiler Intermediate Representation. A unified IR proposed for extracting Lean4 proofs to multiple backends. Mentioned in Hicks' workshop talk. - **Lean4**: the proof assistant and programming language built on dependent type theory. The subject of this document. - **Lean-EVM**: Nethermind's formal Lean4 model of the Ethereum Virtual Machine. Passes 99.99% of EVM conformance tests. - **LeanSig**: the Rust library for hash-based post-quantum signatures used by gean. Not Lean4. - **LeanSpec**: the Python reference specification of Lean Ethereum. Not Lean4. - **LeanVM**: a minimal zkVM for post-quantum signature aggregation. Not Lean4. - **LMD GHOST**: Latest Message-Driven Greedy Heaviest Observed Subtree. The fork choice rule used by Lean Ethereum (and inherited from Beacon Chain). - **Mathlib4**: the community-maintained library of formalized mathematics in Lean4. - **NARK**: non-interactive argument of knowledge. ARK + Fiat-Shamir. - **Pronic number**: a number of the form `n*(n+1)`. Used in 3SF-mini's justification rules. - **Proof assistant**: software for interactively constructing and checking formal proofs. Lean4, Coq, Isabelle, Agda. - **Proto-array**: the indexed, in-place data structure used by gean's production fork choice. Lives in `forkchoice/protoarray.go`. - **Refinement**: the relationship between two state machines where one is a "more concrete" version of the other. - **Round-by-round knowledge soundness**: the security notion that ArkLib uses for IORs. Implies state-restoration soundness and argument soundness. - **Schnorr identification**: the canonical example of a Σ-protocol. Three messages: commit, challenge, response. - **Σ-protocol (sigma protocol)**: a three-move interactive proof with a particular structure. The simplest argument of knowledge. - **Soundness**: the property that a verification system never accepts a false statement. Non-negotiable. - **Spartan**: a SNARK system based on Sum-Check applied to R1CS. Formalized in ArkLib. - **STARK**: scalable transparent argument of knowledge. Post-quantum, no trusted setup. Reed-Solomon-based. - **State machine**: a model of a system as a set of states plus transitions. The natural framing for consensus. - **STIR**: a successor to FRI with better soundness/cost trade-offs. Formalized in ArkLib. - **Sum-Check protocol**: a foundational interactive proof for proving that a polynomial sums to a known value over a hypercube. Used everywhere in modern SNARKs. - **TCB**: trusted computing base. The set of components that, if buggy, can break the system's guarantees. For a Lean4 proof, the TCB is the kernel + axioms. - **Tactic**: a high-level command in a proof assistant that constructs a (sub)proof. Examples: `simp`, `omega`, `induction`. - **Type theory (dependent)**: the foundation of Lean4. Types can depend on values. - **VCVio**: a Lean4 library for cryptographic reasoning (oracle queries, computational soundness). Used by ArkLib. - **WHIR**: the post-quantum SNARK gean uses for signature aggregation. Reed-Solomon based, FRI-family, hash-based, transparent setup. Used by `xmss/rust/multisig-glue`. - **XMSS**: extended Merkle signature scheme. The hash-based post-quantum signature scheme used by gean (`xmss/rust/hashsig-glue`). ## 40. The user's link bundle, annotated For each URL the user provided, what it is, when to read it, and what to skip on the first pass. ### `https://leanprover-community.github.io/learn.html` **What it is**: the Lean4 community's learning portal. It is an index page pointing at every textbook, tutorial, and reference. **Read first.** Skim it once to know what exists, then go to *Functional Programming in Lean*. Do not try to read everything linked from this page in one sitting. ### `https://lean-lang.org/functional_programming_in_lean/` **What it is**: David Christiansen's *Functional Programming in Lean*. The textbook for **Stage 1** of the curriculum (Part VI). Teaches Lean4 as a programming language, not as a proof assistant. Read chapters 1–5. Skip the IO chapters on first pass. ### `https://lean-lang.org/theorem_proving_in_lean4/` **What it is**: Avigad, de Moura, Kong's *Theorem Proving in Lean 4*. The textbook for **Stage 2**. Teaches the proof side of Lean4. Read chapters 1–7 and the tactics chapter. The chapters on quotients, the axiom of choice, and the elaboration model can wait. ### `https://leanprover-community.github.io/mathematics_in_lean/` **What it is**: Avigad and Massot's *Mathematics in Lean*. The textbook for **Stage 3**. Teaches you how to use Mathlib4 to do real mathematics in Lean4. Read chapters 1–5 and the elementary number theory chapter. The topology and analysis chapters are optional unless you find them interesting. ### `https://lean-lang.org/doc/reference/latest/` **What it is**: the official Lean4 language reference. **This is a reference, not a textbook.** Do not try to read it cover to cover. Open it when you need to look up syntax or a builtin tactic. Use search. ### `https://github.com/leanprover-community/mathlib4` **What it is**: the Mathlib4 source repository. ~1.6 million lines of formalized math. **Browse, do not read.** The right way to use this is via the docs (`https://leanprover-community.github.io/mathlib4_docs/`), which are auto-generated and searchable. Pull the source down to your machine when you need to grep for lemmas. ### Recommended additions (not in the user's original list) - **`https://github.com/Verified-zkEVM/ArkLib`** — ArkLib repo. Read after Stage 4. - **`https://verified-zkevm.org/`** — the umbrella project for the Lean4 + zkEVM work. Read for context. - **`https://leanprover.zulipchat.com/`** — the Lean Zulip. Sign up before Stage 1. - **`https://leanprover-community.github.io/mathlib4_docs/`** — Mathlib docs. Use during Stages 3+. - **`https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.html`** — Justin Thaler's textbook. Read parts of it during Part V. - **`https://toc.cryptobook.us/`** — Boneh & Shoup. Reference for crypto background. - **`https://softwarefoundations.cis.upenn.edu/`** — Pierce's *Software Foundations*. Read Volume 1 chapters 1–8. ## 41. The minimal action checklist If you walk away from this document with nothing else, walk away with this. These are the six things to do tomorrow. 1. **Sign up for the Lean Zulip** (`leanprover.zulipchat.com`). Subscribe to `#new members` and `#mathlib4`. You do not have to post — you have to be able to ask later. 2. **Install elan + Lean4 + the VS Code extension** (Stage 0 of the curriculum). Allocate 1–2 hours, not 5 minutes. 3. **Read `gean/statetransition/justifiable.go` and write down every invariant in plain English.** Not in Lean4 — in English. This is the file you will eventually verify, and the English version is 80% of the work. 4. **Bookmark the four resources you will live in**: *Functional Programming in Lean*, *Theorem Proving in Lean 4*, *Mathematics in Lean*, and the Mathlib4 docs. 5. **Subscribe to the ArkLib repo** (`github.com/Verified-zkEVM/ArkLib`). Set notifications for new PRs. Start the weekly habit. 6. **Read the four workshop notes referenced throughout this document**: `pq1-07.md`, `pq1-08.md`, `pq2-05.md`, `pq2-08.md`. They are short. They will give you the names and the politics of the field. That is the entire on-ramp. The rest is the curriculum. --- ## A closing note on what this document is not This document is **not** an introduction to Lean4 syntax. It is **not** a tutorial. It is **not** a reference. It is **not** a guarantee that any of the FV work it describes will happen on any specific timeline. Plans change; people leave projects; tooling slips. What this document **is** is a *mental model*. It tells you what the words mean, where the boundaries are, what is real and what is hand-wavy, and what you should do first. With this mental model in your head, you can open *Functional Programming in Lean* on Monday morning and know what you are doing it for and where you are going. That is the only thing the document promises. Good luck. The 2027 timeline is closer than it looks. --- *Document maintained at `/Users/bankat/Documents/protocol/gean-agent/learning/lean4-formal-verification-mental-model.md`. Source material: gean codebase exploration; Lean Week Cambridge 2025 workshop notes at `pm/workshops-and-interops/2025/lean-week-cambridge/`; FORT MODE PQ Devnet hackmd at `https://hackmd.io/@reamlabs/fort-mode-pq-devnet-ream-view`. Last updated: 2026-04-09.*