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

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
• A (somewhat) formally verified implementation of Markdown
• Formally verified CRUD
• Formally Verified [zkVM] Autoprecompiles
• A new software engineering paradigm

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)

Docs

• mathlib4 docs
• LeanSearch
• Loogle

Misc

• CSLib
• lean4-skills
• Lean game server
• Hitchhiker’s guide to formal verification [in Lean]
• Lean metaprogramming
• Insertion sort in Lean with termination proof
• Tutorial: Introduction to Formal Verification with Lean (Part 1)
• From Prompts to Protocols: lean4-skills for AI-Assisted Lean Formalization

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 👇👇