Developing provably correct Rust code with Verus

Developing provably correct Rust code with Verus - 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

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

Developing provably correct Rust code with Verus

How the Verus "program verifier", which automatically checks code against a mathematical specification of its functionality, helps increase security assurance in software projects.

By Bryan Parno

August 31, 2026

7 min read

Share

Share

Copy link

Email

X

LinkedIn

Facebook

Line

Reddit

QZone

Sina Weibo

WeChat

WhatsApp

分享到微信

x

Listen • 10:04 min

Key takeaways

Verus is an open-source automated program verifier for Rust that mechanically checks code against formal mathematical specifications for all possible inputs, going beyond traditional testing to catch corner cases. Developers annotate Rust source code directly with preconditions and postconditions using Rust-like syntax, enabling fast feedback loops (under one second) and allowing AI agents to assist in proof generation. Verus enables mathematical verification of Rust's "unsafe" code blocks and concurrent code with custom locking schemes, re-establishing machine-checked safety guarantees for performance-critical implementations like AWS's Nitro Isolation Engine. Amazon uses Verus to prove correctness of key primitives in critical infrastructure, and the tool has been adopted by open-source projects including certificate validation libraries, data format parsers, and distributed systems like Kubernetes controllers.

Was this answer helpful?

Many open-source and industry software projects, including several here at Amazon , are embracing the Rust programming language, since it provides performance and flexibility similar to that of the C programming language, while its clever type system automatically prevents a variety of bugs and security vulnerabilities. The result is fast code that's more correct and secure than average. However, "more correct and secure" is not the same as "actually correct and secure". For example, in C, accessing an array out of bounds — indexing into an array past the boundary of the memory allotted to it — is a dangerous mistake that can have unforeseeable consequences. In Rust, it will halt the program, which is definitely safer, but a correct program would never perform the out-of-bounds access in the first place. Similarly, Rust cannot guarantee that your program will compute the results you were expecting or that it won't leak the secrets it has access to. That's where Verus comes in.

Accessing an array out of bounds is a dangerous mistake that can have unforeseeable consequences. A correct program would not permit it.

What is Verus?

Verus is an open-source, automated program verifier for Rust. A "program verifier" takes in a formal mathematical specification of how your code should behave and mechanically checks that your code matches that specification for all possible inputs. For example, your code might implement an optimized binary-search algorithm to look for a particular value within a sorted array. The specification might state that when the code successfully returns an index, the corresponding element in the array matches the target value. The verifier checks that this specification holds for all possible input...