Amazon is investing in the Lean Focused Research Organization

AmazonByron Cook, Shawn BiceJul 26, 2026

Announcement

Summary

As AI agents handle high-stakes operational and financial decisions, traditional software testing fails to provide exhaustive correctness guarantees across all possible inputs. Mathematical proof offers deterministic verification that systems cannot behave incorrectly, but requires accessible tooling to function at modern software scale. To address this, Amazon announced substantial long-term financial backing for the Lean Focused Research Organization, representing the largest donation in the organization's history. Internally, Amazon relies on Lean for verifying differential-privacy mechanisms in AWS Clean Rooms, hardware compilation in AWS Neuron, and policy constraints within Amazon Bedrock AgentCore. Developing Lean externally through an open-source research organization provides independent auditability for regulators and accelerates community-driven tooling for neurosymbolic AI safety.

Context

Standard software testing only checks anticipated cases, which is insufficient as AI agents increasingly make high-stakes decisions such as moving money, approving claims, and operating critical infrastructure.

Approach / What changed

Amazon is providing long-term financial support through the largest donation in history to the Lean Focused Research Organization, funding the development of the Lean language and verification tooling as an open, community-governed project.

Takeaways

Amazon uses Lean to verify policy boundaries in Amazon Bedrock AgentCore, differential-privacy protections in AWS Clean Rooms (SampCert), and hardware compilation in AWS Neuron.
Amazon paired an LLM with Lean to prove the correctness of Amazon Aurora's distributed segment repair protocol in a fraction of the time required for manual proof.
Maintaining Lean in an independent, open research organization allows regulators and customers to inspect verification tools while expanding the shared ecosystem of formal proofs and libraries.

Read original post

Related reading

Amazon · Aug 11, 2026
A decade of mathematical certainty: Reflections on the Automated Reasoning Group
Launched in 2016, the AWS Automated Reasoning Group applies mathematical logic, formal verification, and satisfiability modulo theories solvers to prove the correctness and security of cloud systems at scale. Early research prototypes such as Tiros and Zelkova evolved into production tools like Reachability Analyzer, Amazon Inspector, S3 Block Public Access, and IAM Access Analyzer to evaluate network reachability and access policies. Internally, the group has verified foundational infrastructure, including cryptographic libraries, boot code, the Nitro Confidentiality Engine, and an authorization engine handling one billion API calls per second. Requiring precise formal specifications frequently uncovered simpler, more maintainable system designs while establishing guarantees that traditional scenario-based testing cannot provide. Recent initiatives integrate automated reasoning into generative AI workflows, powering Amazon Bedrock Guardrails, agent compliance policies, and requirement verification in Kiro.
Byron Cook
Amazon · May 4, 2026
Building trust into AI
Amazon integrates responsible AI practices across four core model development phases: pretraining, post-training, evaluation, and third-party monitoring. During pretraining, researchers augment training corpuses with specialized safety datasets, multimodality alignments, and learning exercises to teach foundational safety concepts instead of purely filtering harmful text. In post-training, reinforcement learning from human feedback uses human preference rankings, auxiliary-reward models, and independent LLM judges to ensure model outputs adhere to safety policies. For specialized use cases requiring access to sensitive domains like security testing, researchers apply low-rank adaptors to alter model behaviors surgically without retraining base weights. Cross-functional policy teams guide these technical stages by mapping risks against eight responsible AI dimensions and continuously updating behavioral boundaries to reflect evolving regulatory frameworks.
Staff writer
Amazon · Jun 8, 2026
Real-world grounding in agentic AI
Foundation models deployed as physical AI agents face critical risks when natural language hallucinations translate into physical law violations and operational hazards. To ensure physical consistency and reliability, researchers from the University of California, San Diego and Amazon Fulfillment Technology introduced four grounding pillars. Physics-guided deep learning embeds symmetries and differential equations into pretraining to obey conservation laws while reducing dataset requirements. The UQ4CT framework applies mixture-of-experts architectures to produce calibrated uncertainty estimates, cutting expected calibration error by over 25% and halting operations when safety thresholds are breached. Furthermore, the Adapting-While-Learning framework and formal verifiers like Hilbert integrate numerical simulators and interactive proof systems to enforce mathematical and scientific correctness.
Rose Yu
Amazon · May 27, 2026
Amazon Research Awards recipients announced
Amazon Research Awards has announced 70 award recipients across 49 universities in 11 countries for its fall 2025 funding cycle. The funded research spans six distinct tracks: AI for Information Security, Agentic AI, Automated Reasoning, AWS Cryptography, Cybersecurity and Anti-Abuse Technologies, and Sustainability. Each selected academic team receives unrestricted financial grants, AWS Promotional Credits to access specialized cloud AI and machine learning services, and access to more than 700 Amazon public datasets. Awardees are paired with an Amazon research contact who provides advisory support, consultation, and access to company training sessions. Furthermore, the program explicitly encourages recipients to publish their discoveries, deliver presentations at Amazon offices worldwide, and release associated software implementations under open-source licenses.
Amazon Research Awards team