Formal verification in Lean

tl;dr: A bunch of resources I hope to get to.

Cryptography

• Verified-zkEVM
  • VCVio
  • ArkLib
  • clean zkDSL
• zkLean: A DSL for ZK statement verification
• Paper: SoK: Computer-aided cryptography
• Paper: SSProve: A foundational framework for modular cryptographic proofs in Coq
• AICR: A living, AI-native record of open cryptographic problems, attempts, partial progress, and verification

Software engineering in Lean

• Why lean is faster than Rust
  • Lean proved this program was correct; then I found a bug.
• Just Lean: a verified, fast sort
• Sort in Rust, prove in Lean example
• Lean-ing into Software Engineering
• (somewhat) formally verified implementation of Markdown
• Formally verified CRUD
• Formally Verified [zkVM] Autoprecompiles
• A new software engineering paradigm
• evm.asm: EVM implemented in RISC-V assembly and proved against a Lean spec of RISC-V and a Lean spec of the EVM.

Rust (Non-Lean)

• Verus: Verified Rust for low-level systems code
• Creusot: a deductive verifier for the Rust programming language
• Aeneas: translation from Rust’s MIR internal language to a pure lambda calculus
  • Often used to “compile” a subset of Rust to Lean

Logic

• Propositional logic, $p \wedge \neg p$ type of thing; no quantifiers; no predicates
• First-order logic, $\exists y, \forall x, P(x, y)$; quantifiers and predicates
• Second-order logic, $\exists P, \forall x. P(x)$; more expressive than first-order logic (quantifies over predicates too)
• Intuitionistic logic (constructive logic)
  • Does not assume the law of excluded middle (LEM): i.e., $p \lor \lnot p$ (a.k.a., $p$ or not $p$) is not an axiom; you must actually prove either “$p$” or “not $p$”
  • …nor double negation elimination (DNE): i.e., $\lnot\lnot p \to p$ is not an axiom
    • The converse, introduction, does hold: $p \to \lnot\lnot p$ is constructively provable
  • But… but! If you assume one, you can prove the other one is implied. e.g., assuming LEM, can prove constructively that DNE holds
    • In Lean, it so happens you tend to assume a particular flavor of the axiom of choice, which implies LEM, which implies DNE
• Curry-Howard correspondence

Docs

• mathlib4 docs
• LeanSearch
• Loogle

Misc

• CSLib
• lean4-skills
• Hitchhiker’s guide to formal verification [in Lean]
• Lean metaprogramming
• From Prompts to Protocols: lean4-skills for AI-Assisted Lean Formalization

Tutorials

• Lean Lab, by Alexander John Lee
• Lean game server
• Insertion sort in Lean with termination proof
• Tutorial: Introduction to Formal Verification with Lean (Part 1)

Questions

Probability

How good is Lean at modeling probabilistic games in cryptography?

High-performance code

Need two things that are in tension:

• high performance code
• code that is provable against the spec

e.g., if the code is in (some subset of) Rust, we can translate it to Lean using Aeneas (see above). But not sure how well this works in practice. Also, not sure how much TCB this involves.

References

For cited works, see below 👇👇