zkGolf is a competition for building the cheapest zero-knowledge circuits, with correctness proved in Lean 4.

LeanDY marries type-based and trace-based protocol proofs in Lean, finally making symbolic verification wear two hats instead of one.

Repo with Python/Sage/Lean code, datasets, and commands to reproduce HAWK class-group experiments and formal checks.

Need Yul semantics in Lean? This repo gives big-step semantics, an executable interpreter, and a verified Fibonacci demo.

zk.golf turns circuit golf into a competition, with Lean proofs and a Clean-based submission pipeline.

An essay arguing multi-agent codegen dies on vague specs, and only verification or invariants save it, as usual.

Lean's ArkLib post, formal verification for SNARKs and arguments of knowledge, for people who enjoy proving proofs.

Lean PR proving Halo2 permutation/lookup soundness and union-find permutation construction, because papers enjoy grand products.

The annoying bit was an implicit carry bound, and they proved a Plonky2 U32AddManyGate in Lean after exporting Rust constraints.

Vitalik’s take on formal verification, with Lean examples and a sober look at where end-to-end proofs still blow up.