In 2016 a small research team at Amazon announced our presence to the world with the launch of the Automated Reasoning Group (ARG). Our vision was bold: use mathematical logic to not just test AWS systems but to prove, with mathematical certainty, that they work correctly.
In the intervening decade, we’ve gone from exploring whether advances in formal verification could mitigate previously intractable problems — at AWS scale — to building systems fundamental to how AWS approaches security and reliability. Our group’s production services process billions of queries daily.
This is a look back at how we applied cutting-edge formal-verification and program analysis techniques to Amazon's unique challenges. We were motivated by the belief that real-world security and infrastructure problems could be solved with mathematical rigor at AWS scale. After all, tools like the ones we were researching had already proven successful at places like Intel and NASA. What we didn't fully anticipate was just how broadly applicable these techniques would become.
From demos to production at scale
When we held our first ARG Demo Day in 2016, we showcased several ambitious projects to AWS Security. Each represented a different approach to the same fundamental question: how can we use mathematics to prove that our systems are secure and correct? The answers presented that day laid the groundwork for systems that continue to play significant roles for AWS and our customers in 2026.
Sean McLaughlin gave a presentation titled “Automatic tools for reasoning about virtual private clouds (VPC)”. He noted that the growth of VPC networks had led to an increase in the demand for automated-reasoning solutions capable of identifying misconfigurations or security vulnerabilities. His answer was “a tool called Tiros, which, just simply put, answers questions about your network.”
Tiros became the foundation of a network security analysis feature in the Amazon Inspector service, which is used by millions of customers building applications in the cloud. Tiros is also used within AWS to automate the checking of compliance certification and adherence to security invariants for many AWS services. Today it powers both Amazon Inspector and Reachability Analyzer. This work also split off and became Zelkova, which uses automated reasoning to analyze policies and the future consequences of policies. Zelkova powers tools such as S3 Block Public Access and IAM Access Analyzer, among many others.
Similarly, a presentation given that day on the use of deep automatic analysis for crucial infrastructure turned into the work that we did to prove the correctness of our TLS handshake and other properties of cryptographic, storage, and virtualization code.
Our vision was bold: use mathematical logic to not just test AWS systems but to prove, with mathematical certainty, that they work correctly.
Even some of the smaller-scale projects we spotlighted went on to have an outsized impact. When we presented our work on deductive verification for high-value infrastructure, it largely applied to the deepest parts of our cryptographic protocols. Today the importance of that work has grown enormously, fueled by the rise of proof assistants — automated tools such as Lean (created by Leo de Moura, a senior principal scientist on our AR team) that help users develop formal proofs. We can now pair those tools with language models to find proofs for more and much bigger systems. In fact, the proof we announced for the Nitro Confidentiality Engine is evidence of this. It is also the basis of our proof of the AWS policy interpreter and more recent work proving the correctness of our cryptographic foundations.
Mathematical guarantees customers rely on
Over the past decade, ARG's research prototypes have evolved into services that millions of AWS customers use every day.
IAM Access Analyzer uses Zelkova to help customers like USAA and GoTo identify unintended access to their resources. Instead of hoping security policies are configured correctly, customers get mathematical proof of what their policies actually permit.
Reachability Analyzer, built on the Tiros service we demonstrated in 2016, helps customers understand network connectivity without sending a single packet. Rather than testing configurations, it mathematically analyzes all possible network paths to answer whether a destination is reachable and, if not, what the blocking component is.
Amazon Bedrock Guardrails with Automated Reasoning checks brings mathematical verification to generative AI. The feature helps prevent AI hallucinations by using formal logic to validate that model responses comply with defined policies — delivering up to 99% verification accuracy.
These customer-facing services share a common foundation: they use satisfiability modulo theories (SMT) solvers and other automated-reasoning techniques to provide mathematical guarantees about system behavior, going far beyond what traditional testing can achieve.
Proving the infrastructure beneath the cloud
While customer-facing tools demonstrate automated reasoning's practical value, some of our most challenging work has focused on AWS's internal infrastructure — systems that must be correct because millions of workloads depend on them.
We've used automated reasoning to prove the correctness of much of our infrastructure, including
- The AWS Nitro Isolation Engine
- Cryptographic implementations like s2n-bignum
- Boot code running in AWS data centers
- Storage systems like S3
In one particularly ambitious project, we proved correct and seamlessly replaced our entire authorization engine, which handles one billion API calls per second. We used specifications and proofs and verified the new engine against quadrillions of production authorizations.
These internal verification efforts demonstrate how automated reasoning can provide mathematical certainty about the most foundational layers of cloud infrastructure.
An unexpected discovery
Perhaps the most surprising finding from our decade of work is that automated reasoning doesn't just make systems more secure; it often makes them more efficient and easier to maintain. When teams must write precise specifications for verification, they often discover simpler, more elegant solutions to their problems.
Automated reasoning doesn't just make systems more secure: it often makes them more efficient and easier to maintain.
This is partly because of the systemic approach enabled by automated reasoning. Rather than focusing on validating system behavior under specific scenarios, automated reasoning uses logic to verify system behavior under any possible scenario. Rather than considering all possible input scenarios and how they might go wrong, we define how the system should work and identify the necessary conditions for that behavior. Then we can verify that those conditions are true by using mathematical proof. In other words, we can verify that the system itself is correct.
This discovery has validated our belief that mathematical rigor and practical engineering aren't opposing forces — they're complementary. The discipline required for formal verification frequently reveals opportunities for simplification that might otherwise remain hidden.
Building the foundation for agentic AI
The research we began a decade ago has uniquely positioned us for the next era of AI development. Our work in distributed systems and critical code verification laid groundwork that now applies directly to verifying AI-generated code. Meanwhile, our research into misconfigured AWS policies and VPC networks now helps verify the correctness of AI-generated content.
Evidence for this evolution is found in some of our recent launches. Amazon Bedrock Guardrails with Automated Reasoning checks represents a significant milestone by moving from tools requiring deep expertise to capabilities embedded directly in services builders use every day.
Policy in Amazon Bedrock AgentCore uses automated reasoning to set clear boundaries for agent actions, ensuring agents stay within defined compliance boundaries while operating autonomously. Teams can use natural language to specify which tools and data agents can access, and when integrated with AgentCore Gateway, the system checks policies in milliseconds.
In Kiro, an agentic development environment, we released a requirements analysis capability that uses automated reasoning to prove that there are no contradictions, ambiguities, and gaps in the software requirements before code is written, increasing code accuracy and preventing future debugging cycles. The team building Kiro also uses automated reasoning to check if the underlying AI-generated code works correctly before releasing the feature publicly.
As AI agents become more autonomous and take on more complex tasks, the need for mathematical guarantees about their behavior becomes critical. When AI agents suggest code changes to systems with formal specifications, those systems can automatically verify those changes against mathematical proofs. Automated reasoning provides a path to building AI systems that are not just powerful but provably safe and reliable.
A decade of collaboration
This work wouldn't be possible without the talented team we've built and the customers who've trusted us to help secure their critical infrastructure. Across AWS, teams are continuing to expand automated-reasoning capabilities.
Senior principal scientist Daniel Kroening and his team in Annapurna are advancing hardware verification. Senior applied scientist Nadia Labai is pioneering auto-formalization research, teaching AI systems to convert natural language into formal mathematical proofs. Principal applied scientist Tristan Ravitch and his team in AWS Security launched Peri to automatically track data flow across all accounts in AWS and Amazon, with zero onboarding for service teams.
These efforts position AWS to make the next decade of automated reasoning just as transformative — if not more so — than the first.
What we've proven
Ten years later, I'm incredibly excited about what we've accomplished. We've proven that automated reasoning delivers measurable value at every layer: from preventing configuration errors to providing mathematical guarantees about AI system behavior. We've demonstrated that mathematical rigor and practical engineering can work together to solve real customer problems at scale.
The journey from that first demo day in 2016 to where we are today exemplifies AWS's commitment to transforming academic advances into services customers rely on daily. We've built a foundation of trust through mathematical certainty — and that foundation will be essential as we navigate the next decade of AI innovation.
Here's to the next 10 years.
