How academic collaboration delivers real-world security to Amazon customers

How academic collaboration delivers real-world security to Amazon customers - Amazon Science

Close

Close

Social

bluesky

threads

twitter

instagram

youtube

facebook

linkedin

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

Email

X

LinkedIn

Facebook

Line

Reddit

QZone

Sina Weibo

WeChat

WhatsApp

分享到微信

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...