Amazon is investing in the Lean Focused Research Organization

Amazon is providing substantial, long-term financial support to the Lean Focused Research Organization (FRO), the team building the Lean programming language. Amazon said this is the single largest donation in the FRO's history.

According to Amazon, Lean is a programming language with the potential to make correctness proofs practical at the scale of modern software. The company said testing only checks cases developers thought of, while mathematical proof shows with certainty that a system cannot behave incorrectly regardless of inputs.

Amazon said Lean has spawned a community of users across mathematics, computer science, physics and other fields. It led to Mathlib, described as a comprehensive library of formalized mathematics. Amazon also said AI generation of formal proofs in Lean has been a key method for training models with lower error rates, to the point that they now produce correct solutions to research-level problems.

Amazon said Lean-based verification is used in Policy in Amazon Bedrock AgentCore, which proves the correctness of the policy language that keeps AI agents within specified boundaries. It also underpins correctness proofs for SampCert, which provides mathematical guarantees that differential-privacy protections in AWS Clean Rooms are sound, and AWS Neuron, for compilation to Amazon's AI acceleration chips. Amazon said one scientist recently used an LLM with Lean to prove the correctness of Amazon Aurora's segment repair protocol in a fraction of the time it would have taken manually.

Amazon said it chose to support Lean development through the independent FRO rather than internally because customers, auditors and regulators can independently inspect and validate work done in community-governed tools. It added that Lean becomes more useful as its developer community grows, providing more libraries, tooling and formalized proofs.