A decade of mathematical certainty: Reflections on the Automated Reasoning Group

Amazon's Automated Reasoning Group (ARG) marked a decade since its 2016 launch, describing how its formal-verification research moved into production services used across AWS. The group said its production services process billions of queries daily.

The group traced its origins to a 2016 ARG Demo Day presented to AWS Security. Sean McLaughlin's presentation on tools for reasoning about virtual private clouds introduced Tiros, described as a tool that answers questions about a network. Tiros became the foundation of a network security analysis feature in Amazon Inspector, is used within AWS to automate checking of compliance certification and security invariants, and today powers Amazon Inspector and Reachability Analyzer. The work also split off into Zelkova, which analyzes policies and their future consequences and powers tools including S3 Block Public Access and IAM Access Analyzer.

ARG said its prototypes became services used by millions of customers. IAM Access Analyzer uses Zelkova to help customers including USAA and GoTo identify unintended access to resources. Reachability Analyzer, built on Tiros, analyzes all possible network paths without sending packets to determine whether a destination is reachable and, if not, the blocking component. Amazon Bedrock Guardrails with Automated Reasoning checks applies formal logic to validate that model responses comply with defined policies, which ARG said delivers up to 99% verification accuracy. These services use satisfiability modulo theories (SMT) solvers and other automated-reasoning techniques.

The group said it proved the correctness of internal infrastructure including the AWS Nitro Isolation Engine, cryptographic implementations such as s2n-bignum, boot code running in AWS data centers, and storage systems like S3. In one project, it proved correct and replaced its entire authorization engine, which handles one billion API calls per second, verifying the new engine against quadrillions of production authorizations.

ARG also described applying automated reasoning to agentic AI. Policy in Amazon Bedrock AgentCore sets boundaries for agent actions, and when integrated with AgentCore Gateway the system checks policies in milliseconds. In the Kiro agentic development environment, a requirements analysis capability proves there are no contradictions, ambiguities or gaps in software requirements before code is written.

The group cited Lean, a proof assistant created by senior principal scientist Leo de Moura, and said proof assistants can now be paired with language models. It named Daniel Kroening's team in Annapurna advancing hardware verification, Nadia Labai's auto-formalization research converting natural language into formal mathematical proofs, and Tristan Ravitch's team in AWS Security launching Peri to track data flow across all accounts in AWS and Amazon with zero onboarding for service teams.