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

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

Misc

• CSLib
• lean4-skills
• Lean game server
• 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 👇👇