Featured repo
clean
Formally verified zkEVM in Lean 4, built for Ethereum Foundation with a focus on auditability.
Lean 4 zkEVM Formal proofs
★ 1.2k ⑂ 78 Updated 3d ago
Snapshot
clean / circuits / addition8.lean
1
def circuit := do
2
let x ← witnessField (F := F pBabybear) fun _ => 246
3
let y ← witnessField fun _ => 20
4
let z ← Gadgets.Addition8.circuit.main { x, y }
5
Gadgets.Addition8.circuit.main { x, y := z }
Lean MIT License