How academic collaboration delivers real-world security to Amazon customers
Captured source
source ↗How academic collaboration delivers real-world security to Amazon customers - 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
AGI Labs
Meet the team building useful AI agents.
Amazon Nova
Try Amazon’s frontier foundation models.
Code and datasets
AGI Labs
Meet the team building useful AI agents.
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
How academic collaboration delivers real-world security to Amazon customers
An early meeting between Amazon scientists and Stanford researchers led to cvc5, an open-source tool now powering approximately one billion automated-reasoning checks across AWS every day.
By Staff writer
February 4, 2026
4 min read
Share
Share
Copy link
X
Line
QZone
Sina Weibo
分享到微信
x
On July 16, 2018, Amazon distinguished scientist Byron Cook was giving a keynote at the Federated Logic Conference (FloC) at the University of Oxford, a computer logic gathering held every four years since 1996.
Byron Cook: Formal Reasoning about the Security of Amazon Web Services
In the keynote, Cook described how his team was using an open-source software tool called cvc (cooperating validity checker) to identify logic problems in code and fix them. Sitting in the audience was Stanford University professor Clark Barrett, who had been working on cvc for almost 20 years. Cvc had been developed to analyze verification problems encoded as satisfiability modulo theory (SMT) problems. SMT is a mainstay of formal methods — the use of automated reasoning to prove that a program or system will behave as intended. By applying SMT at scale, cvc can detect logical errors in code and in systems such as those used for authentication and access management. “I was kind of stunned. It was really exciting,” Barrett says. “And this really started with this exciting moment of realizing, Hey, our work is being used by Amazon.” The encounter between Cook and Barrett ultimately led to a years-long research collaboration that culminated in Barrett’s becoming an Amazon Scholar in 2023. Initially, Amazon provided small grants to Barrett’s lab at Stanford’s School of Engineering through the Amazon Research Awards program; those grew into larger funding commitments as the research progressed. This funding supported foundational research that — together with deep technical collaboration between the two teams — enabled the development of cvc5, the latest version of the open-source software. Cvc5 has delivered significant value for both Amazon customers and the broader industry, while simultaneously advancing academic research. As one example, cvc5 is used in Automated Reasoning checks, a new Amazon Bedrock feature that verifies natural-language content against organizational policies. It powers access-policy analysis tools, including Identity and Access Management (IAM) Access Analyzer , a service that helps customers securely manage access to AWS resources. More recently, Amazon has begun deploying cvc5 for specification analysis and test generation in Kiro, a new agentic development environment. Across these applications, cvc5 now processes approximately one billion solver calls every day, enhancing security, reliability, and durability for AWS customers.
How Academic Collaboration Delivers Real-World Security to Amazon Customers
A meeting of…
Excerpt shown — open the source for the full document.
Notability
notability 1.0/10Routine corporate blog, no release or traction
Amazon (Nova) has a writing signal matching safety and policy, product and customer.