Cryptography agenda ZuBerlin 2025

17th of June (Tuesday)

• 16:20 Talk: Formal Verification. By Eduardo Bonilha (Main stage)

1. whoami

• Eduardo, like maths, developer (mention I built a verifier?)
• works at stealth MEV company
  

2. why am I doing a talk on this topic?..

2. why am I doing a talk on this topic?..

wait this guy doesn't even work on formally verifying zkVMs?

am I being scammed?

who let this guy in?

wait, he's saying exactly what's written on the slides?

I think I might leave...

theorem bell.recurrence (n: ℕ) :
  bell (n + 1) = (Finset.range (n + 1)).sum (fun k => Nat.choose n k * bell k)

def partition.insert_recurrence
  (x: X)
  (x_not_in_S: x ∉ S):
  partition (insert x S) ≃ Σ (s : S.powerset), partition (S \ s)

theorem bell.eq_partition_count:
  ∀ n : ℕ,
  ∀ S : Finset X,
    S.card = n → bell n = partition.count S

• I genuinely think automated theorem provers/proof assistants are technology as transformative as AI
• because it's the solution to the slop-topia LLMs coding would bring us to
• some people who low-key kinda agree with this
  
  

1. cryptography needs formal verification, maybe more than anything else
   1. because it's tricky
   2. because it's critical

2. programmable cryptography, especially so
   1. it's going to be used by non-formally trained practicioners of cryptography
   2. going to be deployed across a variety of sensitive protocols

3. I had this existential fear where it seemed hard to completely trust zkVMs

   1. they all depend on complex compiler pipelines
   2. soundness bugs are catasthropic if unnoticed (and hard to notice)

4. so I was invested in this and wanted to figure this out

3. brief intro to zkVMs

3. brief intro to zkVMs

1. nah you guys got this

3. brief intro to zkVMs

1. nah you guys got this
2. ok ok, what's important about them for this talk is that:

1. they verify traces of computation
   • (this sublety is going to be part of an elegant analogy later)

trace of a n-step computation
    [
             (state_0, instruction_0),
        ..., (state_i, instruction_i),
        ..., (state_n, it's  o v e r)
    ]

2. most of them target RISC-V
3. and thus they model von Neumann architecture machines

4. "brief" intro to formal verification

1. what even is formal verification?
2. formal model -> prove properties

curry-howard babyyy

proof carrying-code (PCC)

structure Fin (n : Nat) where
  /-- Creates a `Fin n` from `i : Nat` and a proof that `i < n`. -/
  mk ::
  /--
  The number that is strictly less than `n`.

  `Fin.val` is a coercion, so any `Fin n` can be used in a position where a `Nat` is expected.
  -/
  val  : Nat
  /--
  The number `val` is strictly less than the bound `n`.
  -/
  isLt : LT.lt val n

proof carrying-code

@[ext] structure partition (S: Finset X) where
  
  family : Finset (Finset X)
  
  covers: family.biUnion id = S
  
  non_empty: ∀ c ∈ family, c ≠ ∅
  
  disjoint:  ∀ c ∈ family,
             ∀ d ∈ family,
                c ≠ d → Disjoint c d

5. what does it actually mean to formally verify a xzkVM

1. soundness & completness
   • equivalence between circuit & reference implementation/spec
2. security proof of the ZK construction (the so called "backend")
3. certified compilation pipeline
   • circuit -> constraints
   • constraints -> prover & verifier
     • (prover can include witness gen)
4. (optional, recommended): a way to also prove properties about the programs running on this VM

5.3. certified compilation pipeline

• CompCert
  

• Reflections on Trusting Trust

backdoored compiler source -(compiler)→ malicious binary 

safe source -(malicious compiler)→ backdoored compiler

5.2. verifying cryptographic constructions

• ssprove: state-separating proofs
• concert: smart contract modelling in rocq
• squirrel
• tamarin
• proverif

5.1. soundness & completness

REAL TIME PROVING™, gotta go fast

how do we prove properties of code in random ass langs?
　
　
　
　　　　　　　　　　e x t r a c t i o n

picus (veridise)

• proves soundness with respect to determinism
  • risc0 extracted Keccak circuit and "large parts of our new RISC-V circuit."
  • sp1 extracted addition, boolean ops, binary ops etc
    • they had to translate Plonky3 circuits into LLZK

def determinism (k: SomeOtherInput):
    ∀a, ∀b,
    circuit(a, k) = true
    → verifier(b, k) = true
    → a = b  

　
.　　　
　
　
　
　　
　
　　　　　　　(we can safely
　　　　　　　ignore green arrows)

.　　　　extract artifact after certain compilation step
　　　　　　　　　　　　　≃
　　　　　　　　　　　s t o n k s

(kinda?)

worldcoin semaphore merkle tree batcher (reilabs)

• extracted the gnark constraints to lean (proven-ZK)
• proved following properties:
  • hash correctness (against another reference implementation)
  • determinism (UniqueAssignment)
  • merkle tree ops comply to spec

wanna see what the extracted code looks like?

the theorems... are neat though

axiom reducedKeccak640_collision_resistant :
  ∀x y, reducedKeccak640 x = reducedKeccak640 y → x = y

theorem inputHash_deterministic:
    SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30
        InputHash₁ StartIndex PreRoot PostRoot IdComms MerkleProofs₁
    ∧
    SemaphoreMTB.InsertionMbuCircuit_4_30_4_4_30
        InputHash₂ StartIndex PreRoot PostRoot IdComms MerkleProofs₂
    →
    InputHash₁ = InputHash₂
  := Insertion_InputHash_deterministic

theorem inputHash_deterministic:
    SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30
        InputHash₁ DeletionIndices PreRoot PostRoot IdComms₁ MerkleProofs₁
    ∧
    SemaphoreMTB.DeletionMbuCircuit_4_4_30_4_4_30 InputHash₂
        DeletionIndices PreRoot PostRoot IdComms₂ MerkleProofs₂
    → InputHash₁ = InputHash₂
:= Deletion_InputHash_deterministic

def deletionRoundSemantics
    (Index Item : F)
    (Tree : MerkleTree F poseidon₂ D)
    (Proof : Vector F D)
    (k : MerkleTree F poseidon₂ D → Prop): Prop :=
  if Index.val < 2 ^ (D + 1)
    then if h : Index.val < 2 ^ D
      then Tree.itemAtFin ⟨Index.val, h⟩ = Item ∧
           Tree.proofAtFin ⟨Index.val, h⟩ = Proof.reverse ∧
           k (Tree.setAtFin ⟨Index.val, h⟩ 0)
      else k Tree
    else False

theorem deletionRoundCircuit_eq_deletionRoundSemantics
    [Fact (CollisionResistant poseidon₂)]:
        gDeletionRound tree.root index item proof k
        
        deletionRoundSemantics index item tree proof (fun t => k t.root)

def insertionRoundSemantics
    (Index Item : F)
    (Tree : MerkleTree F poseidon₂ D)
    (Proof : Vector F D)
    (k : MerkleTree F poseidon₂ D → Prop)
    : Prop
:=
  if h : Index.val < 2 ^ D then
    Tree.itemAtFin ⟨Index.val, h⟩ = 0 ∧
    Tree.proofAtFin ⟨Index.val, h⟩ = Proof.reverse ∧
    k (Tree.setAtFin ⟨Index.val, h⟩ Item)
  else False

theorem insertionRoundCircuit_eq_insertionRoundSemantics
    [Fact (CollisionResistant poseidon₂)]
    {Tree : MerkleTree F poseidon₂ D} :
        gInsertionRound Index Item Tree.root Proof k
        
        insertionRoundSemantics Index Item Tree Proof (fun t => k t.root)

/--
Tests the Poseidon implementation automatically derived from the circuit, by
comparing its output on an arbitrary value to a reference value.

The reference value is taken from
<https://extgit.iaik.tugraz.at/krypto/hadeshash/blob/master/code/test_vectors.txt>
-/
theorem poseidon₂_test:
    poseidon₂ vec![1,2] = 0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a
  := by native_decide

jolt

• define jolt lookup table semantics
• extract rust circuit (r1cs) into zkLean
• compare that against Sail risc-v model
• acl2

"towards a verified jolt zkVM" talk

9. let's have a lean pipeline then

i wanna briefly mention powdr

• compiler & IR
• allows defining custom ISAs
• you could host zkVM circuits there and have it automatically optimize it
• autoacc: your constraints → circuit synthesizer → optimized circuit
• it would kinda take a spot akin to LLVM in the toolchain

zk in lean

• zkLib → arklib: verifies modular IOPs
• cLean: circuit zkDSL
• zkLean: zkDSL with verified semantics for lookups (and more?)
• provenZK: analysize extracted circuits
• EVMYulLean: "executable formal model of the evm and yul"
• ...more?
• no need to have more pipeline steps to interop between these
  • any necessary transformations could be verified too
  • could prove equivalences and lift theorems from each other when needed

argument/ix (previous known as lurk)

(remember pcc? now make it zk!)

• implemented lean in lean
• then zk-proved lean (oh yea!)
• could have truly end-to-end certified zkVM
  • contracts could either be in lean
  • or extracted from (e.g.) rust with aenas
• "correct by construction"

argument/ix

• from their readme.md:

[...] hardware based process isolation costs 25%-33% overhead
[...] because we don't know how to safely run applications in protection ring 0.
[...] zkPCC potentially enables more sophisticated software-based process isolation.

note to self: don't forget slides about

• ethproofs
• verified zkEVM
  • 20 mil invested in this

10. conclusion

you can do it too

• opus 4 is quite good at lean
• natural numbers game is quite fun
• curry-howard, type-theory, all so so neat
• contribute to mathlib?

thanks :)