AdaCore and CMU Researchers Announce Collaboration around Formal Verification of Rust for High-Integrity Systems

Collaboration combines AdaCore’s three decades of high-integrity software assurance with Verus, a formal verification tool for Rust.

AdaCore, a trusted provider of software development tools and technologies for safety-critical, high-integrity, and secure systems, today announced a collaboration with CMU researchers working on Verus[1] , an open-source tool for mathematically proving the correctness of Rust code. The collaboration brings together two thought leaders who share one conviction: for software where failure costs lives, money, or missions, testing is not enough; correctness must be proven.

AdaCore’s SPARK Pro has delivered static proof of the absence of runtime errors and proof of functional correctness to avionics, defense, space, rail, and medical programs. Verus brings similar proof capabilities to Rust, extending Rust’s compile-time safety guarantees from memory safety to full functional correctness, with no runtime cost. Together, the two organizations will give high-integrity teams a credible path to proven Rust, whether they are starting a new program with Rust or adding Rust alongside existing Ada, SPARK, C, and C++.

“Demand for formally proven software is growing across the industry, and AI is accelerating this trend from two directions,” said Quentin Ochem, Chief Product Officer at AdaCore. “AI-generated code creates a greater need for rigorous verification, while AI-assisted development makes formal methods more accessible by helping developers produce specifications and proof annotations. With over 15 years of experience bringing formal verification to industrial applications through Ada and SPARK, we’re thrilled to contribute to the Rust ecosystem through our collaboration with the Verus project.”

“Rust’s borrow checker already applies a form of static verification; Verus extends this verification to the properties that actually matter for the high-integrity system you are building. AdaCore has spent decades helping formal proof earn its place in certified, safety-critical programs, and we’re excited to be working alongside their team. By bringing that experience together with the work of the Verus community, we can help verified Rust move from early adopters into the mainstream of high-integrity development.”

Bryan Parno, Kavčić-Moura Professor of Electrical & Computer Engineering and Computer Science at Carnegie Mellon University, and co-developer of Verus

GitHub – verus-lang/verus: Verified Rust for low-level systems code · GitHub

About AdaCore

AdaCore equips developers to create reliable, safe, and secure software. For more than 30 years, AdaCore has provided industrial-grade development and verification tools for Ada, SPARK, C/C++, and Rust, supporting organizations in avionics, defense, automotive, rail, space, and medical systems. AdaCore’s tools are built to meet the most rigorous standards and supported by long-term commitments to ensure continuity and certification readiness.

About Verus

Verus is an open-source verifier for Rust that lets developers prove their code correct using Rust itself as the specification language. It is already used in production at organizations, including Amazon.

•      Zero-cost verification. Verus code is written in three modes: executable (the Rust that ships), spec (mathematical specifications written in a Rust-like syntax), and proof (the arguments that justify them). Spec and proof code are “ghost” code, erased before compilation, so verified binaries carry no runtime overhead and can be compiled with a normal Rust compiler. Proof mode also lets developers manipulate proof-level resources using Rust-like ownership, enabling them to prove, e.g., that code using raw pointers is safe (and correct).

•      Automated reasoning. Verus translates annotated Rust into logical conditions and discharges them with SMT solvers.  This means that humans (and agents) spend less time on low-level proof details.

•      Fast enough for real systems. Verus verifies system code 3 to 100 times faster than prior state-of-the-art verifiers, making proof viable in a day-to-day engineering workflow rather than a one-off research exercise.

•      Beyond functional correctness. The Verus community has developed techniques for proving security properties of parsers, serializers, and cryptographic protocols; reliability properties such as crash safety; and liveness properties for distributed systems.