AdaCore has announced a collaboration with Carnegie Mellon University researchers to advance the formal verification of Rust software, combining its experience in high-integrity systems with the open-source Verus verification tool.
AdaCore has announced a collaboration with researchers at Carnegie Mellon University (CMU) working on Verus, an open-source tool designed to mathematically prove the correctness of software written in Rust.
The collaboration combines AdaCore’s experience in software assurance for safety-critical systems with Verus, which extends Rust’s existing compile-time safety guarantees to include the formal verification of functional correctness.
The initiative is intended to support organisations developing software for environments where failures can have serious safety, financial or operational consequences.
AdaCore’s SPARK Pro technology has been used to verify the absence of runtime errors and prove functional correctness in applications across aviation, defence, space, rail and medical systems.
Verus provides similar verification capabilities for Rust, allowing developers to establish that software meets specified requirements without introducing additional runtime overhead.
Together, AdaCore and the CMU researchers aim to help high-integrity development teams adopt formally verified Rust, whether for new projects or alongside existing Ada, SPARK, C and C++ applications.
Quentin Ochem, Chief Product Officer at AdaCore, said: “Demand for formally proven software is growing across the industry, and AI is accelerating this trend from two directions. 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.”
The collaboration comes as Artificial Intelligence increasingly influences software development, creating opportunities to accelerate coding while also increasing the importance of verifying software behaviour.
Formal verification uses mathematical techniques to establish whether software satisfies defined properties, providing assurance beyond conventional testing.
Rust already incorporates compile-time checks designed to prevent certain classes of memory safety errors. Verus builds on these capabilities by enabling developers to verify additional properties relating to how software functions.
Bryan Parno, Kavčić-Moura Professor of Electrical & Computer Engineering and Computer Science at Carnegie Mellon University and Co-developer of Verus, said: “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.”
The collaboration is intended to make formal verification more accessible to developers working with Rust while supporting its adoption in high-integrity software development.
Verus is available as an open-source project at https://github.com/verus-lang/verus.
