Dr. Achermann and co-authors win Distinguished Artifact Award at top systems conference

One of the biggest challenges in building complex software systems is ensuring they are free from critical errors.

Traditional software testing methods will reveal bugs, but testing alone can’t guarantee the absence of errors. Software verification tools such as Verus establish a rigorous, mathematical proof that the software performs according to its specifications.

Making the use of verification more efficient and accessible for system software developers was the goal for no less than 14 research collaborators. The team was led by Andrea Lattuada of the Max Planck Institute for Software Systems (MPI-SWS) and Chris Hawblitzel of Microsoft Research. Others included Dr. Reto Achermann, Assistant Professor at UBC Computer Science, researchers from industry, and those from universities such as Carnegie Melon University, the University of Texas, ETH Zurich, VMware Research and others.

Their paper, “Verus: A Practical Foundation for Systems Verification” won the Distinguished Artifact Award at the 30th Symposium on Operating Systems Principles (SOSP) in Austin, Texas in early November of 2024.

This accolade highlights the significant advances in verification efficiency for system software written in Rust: an emerging system programming language.

Tackling the challenges of software verification

"Verus enables developers to write both the specification and the implementation in Rust," explains Dr. Achermann. “This unified approach allows developers to use a single language not just for coding, but also for writing specifications and proofs.”

Verus leverages Rust’s robust ownership model and builds specialized constructs for handling memory safety and reasoning about concurrent programs, two critical areas where errors frequently occur. By tackling these key aspects of system software, Verus eliminates bugs in areas that have long plagued developers.

An overview of Virus — Figure 1. **Verus Overview as depicted in the paper.** *Verus offers powerful automated and semi-automated reasoning techniques that apply to the full system stack.*

Achermann explains part of their approach, “For example, in VerusSync, access to shared memory resources is guarded by ‘ghost tokens.’ Ghost tokens are a verification construct. In order to access a shared memory resource, the developer must prove possession of the corresponding ghost token before they can access the shared memory resource.” This technique ensures safety and results in efficient code; the ghost tokens are then optimized away when compiling the executable program.

Shared-memory producer-consumer queue — Figure 2. **Depiction of a shared-memory producer-consumer queue**

Verification at 61x the speed

One of Verus’s standout achievements is its unprecedented speed. Verification using Verus is up to 61 times faster than other verification tools, significantly reducing the time needed to verify code. By enabling faster turnaround times, Verus has become more practical for everyday use by developers that now get their verification results in milliseconds.

Microsoft, a key partner in Verus’s development, is particularly excited about the tool’s potential. “This kind of efficiency has a huge impact on the accessibility of verification,” a Microsoft representative commented.

The researchers’ evaluation of Verus as part of their paper also involved many system software projects that were verified using Verus. According to Achermann, some of these projects were ports from previous work in other verification tools, while others were developed from scratch. "We wanted to demonstrate Verus’s versatility, so we used it to verify a wide range of systems.”

SOSP award — SOSP Distinguished Artifact Award

For the co-authors, the Distinguished Artifact Award was both an honour and a pleasant surprise. “Personally, I didn’t expect to win,” Achermann expressed. “We’d put a lot of work into preparing the artifact, especially Andrea Lattuada who was also coordinating our efforts. It was great to be recognized in this way and very rewarding to see all the hard work pay off. We would also like to thank the Artifact Evaluation chairs and the reviewers for their work.” He added that the award shows the tool is usable and the results reproducible. “Other researchers and software developers can download Verus and start building their verified software,” he said.

What’s next?

With their award-winning verification tool in hand, Reto Achermann and some of the collaborators are already looking toward the future. “Our next goal is to use Verus in the context of building a fully-verified operating system.”

Verus’s success through the research is more than just an academic achievement; it represents a practical shift toward more robust, error-free system software by making formal verification faster and more accessible.

For further explanation, listen to this podcast featuring Microsoft Research senior principal researchers Chris Hawblitzel and Jay Lorch.

Another UBC Computer Science researcher was part of a team who won an award at SOSP also: Dr. Mathias Lécuyer et al. won the Distinguished Artifact Honourable Mention Award for their paper: Cookie Monster: Efficient On-device Budgeting for Differentially-Private Ad-Measurement Systems