Amazon is investing in the Lean Focused Research Organization

Amazon Science · 2 months ago · 16

Amazon is providing substantial long-term financial support to the Lean Focused Research Organization, which develops Lean, a programming language designed to create mathematical proofs that verify software correctness with certainty. Amazon has integrated Lean-based verification into systems like Bedrock AgentCore to prove AI agents stay within specified boundaries, and the language is used to verify critical infrastructure including Aurora's distributed protocols and differential-privacy protections. The investment aims to make formal verification accessible to all developers and ensure AI agents remain trustworthy and safe through mathematical guarantees rather than traditional testing alone.