Lean Into Verified Software Development

This article discusses the use of the Lean proof assistant for verification-guided development of Cedar, an open-source authorization policy language from AWS. The authors describe their experience modeling and formally verifying key properties of Cedar's core components using Lean.

Specifically, the article covers:

• A brief introduction to Cedar and its components: the evaluator, authorizer, and validator
• How Cedar uses Lean for verification-guided development by creating executable formal models and proving correctness properties
• A quick tour of modeling and verifying Cedar with Lean, including code examples and details on the proof effort
• Takeaways and tips for using Lean, such as embracing the learning curve, starting simple, and staying flexible
• Resources for learning more about Lean and Cedar