Use Cases

Lean Powers Secure Software at AWS: Cedar's Journey with Verified DevelopmentIn a significant endorsement of formal verification in production software, AWS scientist Emina Torlak and former AWS scientist Kesha Hietala have shared their success using Lean to verify the AWS...Read more

Mathlib: A Foundation for Formal Mathematics Research and VerificationWhen organizations and researchers consider formal mathematics tools, a crucial factor is the availability of a comprehensive mathematical library. Building formal proofs from scratch is...Read more

Aeneas: Bridging Rust to Lean for Formal VerificationAs Rust continues its explosive growth across the software industry, organizations are recognizing that while Rust's memory safety guarantees are valuable, they may not be sufficient for critical...Read more

Formalizing Fermat's Last Theorem in Lean: A Landmark Mathematical ProjectFermat's Last Theorem (FLT) stands as one of mathematics' most famous challenges, taking over 350 years to solve. Now, an ambitious project led by Professor Kevin Buzzard at Imperial College...Read more