AWS bets big on Lean programming language to bring mathematical guarantees to agentic AI

What AWS thinks

Amazon Web Services (AWS) employees Byron Cook and Shawn Bice blogged this weekend on the organisation’s use of Lean and gave the Computer Weekly Developer Network early access to the content of their thoughts on how Lean can be used inside the company to drive it towards being a lean-focused (sorry, we mean Lean-focused) research organisation.

Byron Cook is VP and distinguished scientist at Amazon Web Services (AWS), he is also the founder and leader of the Automated Reasoning Group (ARG) within AWS. Shawn Bice  is VP of AWS AI services at AWS and he also has a lead role in the ARG team, with specialisms in agentic AI reliability and neurosymbolic AI.

Cook and Bice say they want to tell us about an investment the company is making and why they’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,” said Cook and Bice.

Amazon is now providing substantial, long-term financial support to 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.

Mathlib, formalised mathematics library

“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 formalised 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,” explains Cook and Bice.

The pair say that, to them, 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. 

Policy in Amazon Bedrock AgentCore

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,” clarifies Cook and Bice.

Hey Amazon, why so open?

If you’re wondering why Amazon would want Lean developed in the FRO, outside of Amazon, the AWS automated reasoning gurus have a response.

They say that it’s “easier to trust a proof when you can evaluate the tools behind it yourself,” and in this case we see that 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, conclude Cook and Bice.

They say, through openness, Lean becomes “more useful as its developer community grows” and that’s a community that includes AWS – as the work here ends up providing more libraries, more tooling, and more formalized proofs for everyone.

Deep dive with AWS

AWS’ Cook: Provable correctness has been central to our safety strategy for a decade.

The Computer Weekly Developer Network (CWDN) spoke to AWS for more and sat down with Byron Cook, [who, as noted above is] distinguished scientist, VP, and founder of the Automated Reasoning Group at AWS – and Leonardo de Moura, founder and chief architect of the Lean programming language and senior principal applied scientist for Automated Reasoning at AWS.

CWDN: What real-world failure mode convinced AWS that testing alone is no longer sufficient for agentic AI systems?

Byron Cook: Provable correctness has been central to our safety strategy for a decade. In 2014, AWS made a deliberate decision to invest in automated reasoning for security, and we saw early in generative AI that the same approach would be essential for AI agents taking autonomous action in the real world. We’re committed to building AI that customers can trust and verify with mathematical guarantees. 

CWDN: Beyond Bedrock AgentCore, where else across AWS’s stack will Lean-based mathematical proof be applied to agent behaviour next?

Byron Cook: We’ve already extended Lean-based proofs to verify differential-privacy guarantees, compilation correctness for our custom AI chips, and the durability protocols underpinning our most critical databases. We’re also building Strata, a Lean framework for defining programming language semantics, which lets us verify properties of the code that agents generate and execute on their own. As agents become more capable, proof needs to follow them across every layer from the silicon they run on, to the protocols they depend on, to the code they write.

CWDN: What’s the worst-case scenario you’ve witnessed when an unverified AI agent operated without formal correctness guarantees?

Byron Cook: The scariest failures are the silent ones where an agent looks correct on the surface but harbours a subtle logical gap in its policy, meaning it’s technically authorised to do something its designers never intended. You only discover these when they’re exploited, and by then the action is irreversible. Formal verification eliminates this structural risk because it goes beyond just checking for known bugs by proving no such risk can exist.

CWDN: How does formal proof in Lean differ practically from conventional automated testing when verifying an AI agent’s policy boundaries?

AWS’ de Moura: Exhaustive testing of a complex distributed protocol would, in many cases, take longer than the lifetime of the sun – with symbolic reasoning in Lean, a query can often be resolved in seconds.

Leonardo de Moura: Traditional testing samples a finite number of scenarios, whereas a proof in Lean covers every possible execution simultaneously: if it compiles, there are no counterexamples. You state the property you care about, such as “this agent cannot access data outside its authorised scope,” and the proof guarantees it holds universally, not probabilistically. With AI now helping construct these proofs, what used to require months of specialist effort can happen in a fraction of the time. 

CWDN: Can you share figures (or insight) on how much faster Lean-assisted proof was versus manually verifying Aurora’s segment repair protocol?

Leonardo de Moura: Exhaustive testing of a complex distributed protocol would, in many cases, take longer than the lifetime of the sun. With symbolic reasoning in Lean, a query can often be resolved in seconds. Before AI-assisted proof, verifying a protocol at that level of complexity could take an order of magnitude more effort than writing it. Now, the engineer specifies what must hold, the AI constructs the argument for why, and Lean certifies every step, which makes formal verification practical for production systems. 

CWDN: Why was it essential that Lean’s development sit inside an independent FRO rather than remain an internal AWS project?

Leonardo de Moura: Lean’s strength comes from its global community of contributors across mathematics, computer science, and physics building a shared library of formalized knowledge. An independent nonprofit ensures that community keeps growing.

Byron Cook: Lean becomes more powerful with every contributor where every formalised proof, every library, and every tool that the community builds make the next verification project faster and more capable for everyone. Building in the open also gives users and auditors direct visibility into the toolchain, increasing trust.

CWDN: What’s the one statement you’d want developers to remember about why mathematical proof matters for agentic AI’s future?

Byron Cook: Probably correct AI isn’t good enough. To have trustworthy and safe AI, organisations, developers, and users need provably correct AI. Mathematical proof gives certainty that a system cannot misbehave, and as AI agents take on higher-stakes autonomous decisions, that certainty must become the standard.