🔹 1. Foundational Ideas

• Formal verification ensures software correctness by proving properties of code mathematically.

• Mike Dijkstra’s quote:

  “Testing can only show the presence of bugs, not their absence.”

  Emphasizes the limitation of traditional testing.

🔹 2. Unified Language for Coding and Proving

• In Lean, code and proofs are written in the same language—no need for separate spec/code languages.
• You verify your code directly in the same environment.

🔹 3. Case Studies and Real-World Use

🟠 Amazon Web Services (AWS)

• Uses Lean to model its IAM policy language (written in Rust).
• A model is built in Lean to verify correctness.
• Differential testing: The model and actual implementation are tested on identical inputs.
  • If outputs differ, there's a bug either in the model or code.

🟠 Differential Privacy Project (Jean-Baptiste Tristan, AWS)

• Goal: Add noise to data while preserving utility and ensuring privacy.
• Verified a discrete Gaussian sampler in Lean:
  • Found bugs in the original academic implementation.
  • Resulted in a faster and bug-free implementation.
  • Enabled safe optimization due to formal guarantees.

🔹 4. Lean + Cryptography

🟣 Microsoft’s Project Iineos

• Rust code for cryptography is translated to Lean using a tool.
• Verifies the translated code using Lean's theorem-proving capabilities.