Amazon is investing in the Lean Focused Research Organization - Amazon Science
Close
Close
Social
bluesky
threads
youtube
github
rss
Menu
Research
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
News & blog
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
Collaborations
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Resources
Code and datasets
Amazon Nova
Try Amazon’s frontier foundation models.
Code and datasets
Amazon Nova
Try Amazon’s frontier foundation models.
Careers
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Search
Submit Search
Automated reasoning
Amazon is investing in the Lean Focused Research Organization
As AI agents take on higher-stakes decisions, Lean programming language makes it possible to mathematically prove they will behave safely.
By Byron Cook, Shawn Bice
July 26, 2026
2 min read
Share
Share
Copy link
Line
QZone
Sina Weibo
分享到微信
Key takeaways
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.<br>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.<br>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.
Was this answer helpful?
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...