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