亚马逊长期资助 Lean FRO，用形式化证明保障 AI 智能体安全

As AI agents take on higher-stakes decisions, Lean programming language makes it possible to mathematically prove they will behave safely.

Amazon is providing long-term financial support to the Lean Focused Research Organization (FRO) to advance Lean, a programming language that enables mathematical proofs of software correctness; Amazon uses Lean-based verification across multiple products including Bedrock AgentCore for agentic safety, SampCert for differential-privacy guarantees, and AWS Neuron for AI chip compilation, with scientists using LLM-Lean combinations to prove complex distributed protocol correctness; Amazon supports Lean's development through the independent Lean FRO rather than internally to ensure transparency and trustworthiness, allowing customers, auditors, and regulators to independently validate proof tools for safety-critical AI applications

We want to tell you about an investment we're making and why we're excited about it. As AI agents increasingly make decisions that move money, approve claims, and operate critical infrastructure, the standard approach to software testing is no longer sufficient. Testing checks the cases you thought of, but there is a fundamentally different approach: mathematical proof, which shows with certainty that a system cannot behave incorrectly, no matter what inputs it gets.

Lean is a programming language with the potential to make correctness proofs practical at the scale of modern software. Amazon is now providing substantial, long-term financial support to the team building it — the Lean Focused Research Organization (FRO) — to make proof accessible to every developer in the world. This is the single largest donation in the FRO's history.

Lean has spawned a thriving community of users in mathematics, computer science, physics, and many other fields. It has led to the creation of Mathlib, a comprehensive library of formalized mathematics, which ignited an explosion of further efforts in formalized proofs. And it has had a pivotal role in the development of AI reasoning capabilities: AI generation of formal proofs in Lean has been a key method for training models with lower error rates, to the point that they are now producing correct solutions to research-level problems.

But to us at Amazon, the most exciting thing about Lean is the role it promises to play in agentic safety and neurosymbolic AI: coupling generative AI with Lean's mathematical rigor will help enable verified, trustworthy AI agents. The Lean team drove this vision before the industry caught up, and it’s a vision that is increasingly important to our own strategy for agentic safety. For example, Policy in Amazon Bedrock AgentCore uses Lean-based verification to prove the correctness of the policy language that keeps AI agents within specified boundaries. We haven't seen anyone else offer this type of mathematical guarantee.

Lean also underpins the correctness proofs behind systems such as SampCert (mathematical guarantees that differential-privacy protections in AWS Clean Rooms are sound) and AWS Neuron (compilation to Amazon's AI acceleration chips). One scientist recently used an LLM with Lean to prove the correctness of Amazon Aurora's segment repair protocol, our most durability-critical distributed protocol, in a fraction of the time it would have taken manually. The set of applications is growing fast, and this is just the beginning.

You might wonder why Amazon would want Lean developed in the FRO, outside of Amazon. The answer is that it's easier to trust a proof when you can evaluate the tools behind it yourself. Customers, auditors, and regulators can independently inspect and validate work done in community-governed tools, which is the kind of transparency that safety-critical AI demands.

It also matters internally. Lean becomes more useful as its developer community (which includes our engineers) grows, providing more libraries, more tooling, and more formalized proofs for everyone. For both reasons, we have found it crucial that the foundational work on Lean happens in the open through the Lean Focused Research Organization.

Automated reasoning