Verus: A Practical Foundation for Systems Verification

System software such as file systems, kernels, databases and allocators is low-level, performance-critical and often concurrent, so it is hard to get right. Formal verification can remove whole classes of bugs before shipping, and the community has verified many systems, but the authors note that much of that success needed heroic effort, bespoke logics for one domain (crash safety, for instance) or a loss of expressiveness in exchange for proof automation.

This SOSP 2024 paper (Austin), a collaboration among Carnegie Mellon University, Microsoft Research, VMware Research, MPI-SWS, ETH Zurich, the University of Texas at Austin, the University of Michigan, the University of British Columbia, the University of Wisconsin-Madison and the Weizmann Institute of Science, presents Verus as a foundation for system verification. Verus checks Rust code against specifications written in Rust syntax and sends the proof obligations to the Z3 SMT solver. An earlier OOPSLA 2023 paper by overlapping authors formalized how Verus verifies safe and unsafe Rust with linear ghost types. This one describes the features aimed at systems and evaluates them.

Key terms: a spec function is a pure mathematical function used only in specifications, a proof function is ghost code that helps the solver, and exec code is the ordinary Rust that runs. A trigger is the expression pattern that tells an SMT solver when to instantiate a quantifier. EPR (effectively propositional logic) is a restricted logic that can be checked fully automatically. VerusSync is the new language for describing concurrent ghost state as state transitions. The proof-to-code ratio (P/C) is lines of proof per line of executable code. The trusted computing base here is the top-level specifications, the Verus verifier, the solvers and the Rust compiler.

Worth knowing first: Hoare-style pre and postconditions (requires and ensures), how an SMT solver instantiates quantifiers, and Rust ownership. RustBelt is cited in the related work as the Coq-based, manual verification of unsafe Rust, the contrast to Verus's automated approach. Among other groups' uses of Verus the paper cites a workshop paper on the Atmosphere microkernel. Atmosphere, the later SOSP 2025 paper in this library, also uses Verus, but this paper could not cite it, so that link is my pairing.

• Lean general-purpose automation. Verus turns requires and ensures into verification conditions for Z3 with standard Floyd-Hoare logic and keeps the queries small. Spec functions are pure, total and have no heap access, so they map directly to SMT functions. Memory, bit-vector and nonlinear reasoning are isolated from the main queries, each module's context is pruned of unreachable imports, and triggers are chosen conservatively, as few as possible, with the user encouraged to review them. The authors accept more initial effort on small projects in exchange for scaling to large ones.
• Selective EPR. A developer marks a module #[epr_mode], abstracts a data structure or protocol into EPR (keys as a totally ordered set, say), gets an automatic proof of its inductive invariant and exports the result to the unrestricted original. Verus checks that struct fields are private, that the quantifier-alternation graph is acyclic and enables Z3's model-based quantifier instantiation. The worked example is the IronKV delegation map, whose set operation took about 300 lines of default-mode proof and several days of developer effort.
• Tools for systems idioms. by(bit_vector) reads integers as SMT bit vectors inside one assertion, by(integer_ring) proves congruence relations, by(nonlinear_arith) runs an isolated query with no implicit context, and proof by computation uses a built-in symbolic interpreter (the authors' example is a CRC-32 lookup table whose proof they once gave up on). Rust macros remove repetitive proofs such as marshalling. Each check is automatic, but the main SMT encoding then simply assumes the result, which is why the paper calls these tools trusted.
• VerusSync. It combines resource algebras from concurrent separation logic with a transition language whose syntax follows Ivy. The developer declares fields with sharding strategies (variable, constant, map), writes transitions with enabling conditions and updates, and supplies an inductive invariant. Verus then generates ghost shards and operations that the code uses, tied to atomic memory cells. The authors say a well-formed VerusSync system always corresponds to a resource algebra, so developers need not construct monoids. System-level state machines, such as crash-safety models, are a special case.
• Rust types for memory safety. Memory safety rides on Rust's ownership type checker. Verus accepts a subset of unsafe Rust, with raw pointers guarded by ghost permissions, and rejects features outside it. The authors extended its raw pointer support for these case studies.

The evaluation has two scales. Millibenchmarks compare Verus with Dafny, Low* (the low-level subset of F*), Prusti, Creusot and Ivy on a singly linked list, a doubly linked list (unsafe Rust, because of its cyclic pointers), a memory-reasoning test that updates four lists in one function, and a distributed lock proved in default mode and in EPR mode. They run on an AWS EC2 m5.8xlarge (16 cores, no multithreading, 128GiB) and report medians of 20 runs, plus the time to report an error after removing a precondition from pop or index.

The macrobenchmarks total over 6.1K lines of Rust and over 31K lines of proof. Two are ports that preserve the original algorithms: the IronKV host from IronFleet (Dafny, protocol level skipped) and the Node Replication library NR from IronSync (Linear Dafny). Three are new: an x86-64 page table, a concurrent allocator based on mimalloc, and a persistent circular log for Optane persistent memory, designed for a cloud-scale production storage system (the acknowledgments thank Azure Storage for help with the problem definition and integration). Performance checks are IronKV against IronFleet on a Windows laptop, NR on a four-socket Xeon Platinum 8260 at 0%, 10% and 100% writes, the page table against an unverified one over 100M map and unmap operations, the allocator on mimalloc-bench, and the log against libpmemlog on a 128GiB Optane module.

These are the authors' reported results.

• Linked lists. Verus verifies the singly and doubly linked lists in 0.66 s and 1.15 s. The other tools take 3 to 28 times longer on the first and 24 to 61 times longer on the second, which is where the abstract's 3 to 61× comes from. Creusot's 1.88 s for the first is only the time to a partial result that needs manual completion, and Prusti cannot express the second.
• Failure feedback and memory reasoning. With a precondition removed, Verus, Dafny and Prusti report the error about as fast as they report success, while Low* goes from one second to four and Creusot from one second to twenty. Updating four lists, Verus time grows linearly at about 1.6 ms per push (1.8 ms for doubly linked lists). Dafny grows dramatically, Low* does not return after more than one push, and Prusti and Creusot grow super-linearly.
• Distributed lock. The default-mode inductiveness proof is about 25 lines. The EPR version is automatic but needs about 100 lines of boilerplate, so the authors conclude EPR pays off on complex cases like the delegation map and that Verus should automate the boilerplate.
• IronKV. The port has 1,533 lines of code and 4,509 of proof (P/C 2.9), against 1,923 and 8,070 (4.2) in Dafny. Verification takes 41 s on one core and 18 s on eight, against 445 s and 201 s, and the SMT queries are 17 MB against 352 MB. The authors summarize this as 95% smaller queries and 10× faster verification, with performance comparable to the original.
• NR. The port has 736 lines of code and 5,237 of proof (7.1), against 730 and 7,828 (10.7) in Linear Dafny. Verification takes 17 s on one core and 9 s on eight, against 1,089 s and 228 s, with queries of 22 MB against 2,063 MB. The authors credit VerusSync for most of the proof reduction, and Verus-NR matches IronSync-NR and the unverified original in throughput.
• Page table. 400 lines of code and 5,329 of proof (13.3:1), verified in 63 s on one core and 34 s on eight, using the bit-vector, nonlinear and computation tools 62, 39 and 11 times. Map latency matches the unverified reference, while unmap is much slower because the verified version reclaims emptied page directories, which an unverified variant without reclamation confirms. Larger OS-level benchmarks show negligible differences.
• Allocator. About 3.1K lines of executable code against about 10K in mimalloc, P/C 4.3, a 37-line user-facing specification plus 245 lines of trusted specification for mmap and thread utilities. Verification takes 262 s on one core and 55 s on eight in Figure 9. It supports drop-in use with limits (no realloc, aligned allocations or allocations over 128KiB) and completes 8 of mimalloc-bench's 19 benchmarks, without performance parity.
• Persistent log. 739 lines of code, P/C 3.9, verified in 12 s. It refines an abstract infinite log, makes operations atomic with respect to crashes and protects metadata against corruption up to CRC, and it is integrated into a production codebase as an ordinary Rust crate. After a Serializable trait removed an initial copying overhead, append throughput is comparable to libpmemlog. The authors note this holds even though the verified log computes CRCs and libpmemlog does not, because libpmemlog takes a lock on every append and the verified log uses none.

The paper is candid about the scope of its evidence. It concedes the following.

• The trusted base is real. Results hold relative to the top-level specifications, the Verus verifier, the solvers and the Rust compiler, and Verus accepts only a subset of unsafe Rust. The custom automation is trusted too, and the page table, allocator and log rely on trusted specifications of the MMU, mmap, thread utilities and a CRC crate.
• The evaluation is early. The authors call the 13.3:1 page-table ratio "relatively high" and say it may reflect inexperience or may be inevitable for an OS component. Starting from correct code and finished proofs is, in their words, "overly optimistic", and the true evaluation will come from future projects. The allocator is incomplete and slower than mimalloc.
• Rough edges remain. EPR mode needs about 100 lines of boilerplate even for the simple lock, and its queries are not strictly EPR because of how polymorphic types are encoded, though no correct proof has failed. The IronKV trusted-line counts are, they say, noisy, and conservative triggers cost effort on small projects.

The following points are a reading of the evidence, not claims of the paper.

• Effort is inferred, not measured. The abstract promises faster and cheaper verification, but effort is proxied by line counts and verification time. Apart from the delegation-map anecdote of several days, no person-hours appear, and the "crisp interactivity" of the IronKV port is the porters' own report. The ports also start from finished proofs, and IronKV's protocol level was skipped on the expectation that Dafny and Verus proofs would be similar, which is asserted, not tested.
• Ratios leave out the trusted base. Figure 9's trusted column totals 4,692 lines, close to the 6,119 lines of executable code, and it exceeds the code for the page table (1,117 against 400) and the log (1,284 against 739). The audit burden that remains for humans is not captured by the headline ratio of 5.1.
• Text and table disagree in places. For NR the text claims two orders of magnitude, while Figure 9 gives about 64× on one core and 25× on eight (queries are about 94× smaller). The allocator is verified in "just over a minute" in the text, but 55 s on eight cores and 262 s on one in the table. The Verus total row (6,119 lines of code and 31,231 of proof, behind the 6.1K and 31K headline) is not the sum of the five rows above it, which I read as about 6,586 and 31,691. This review uses the table values.
• The comparisons are the authors' own. Millibenchmarks come from other frameworks' examples, checked with their designers, which is fair, but each millibenchmark number is a median of 20 runs on one machine with no spread, and the low end of the 3 to 28× range is Creusot's partial result. Ivy is named as a comparison tool, yet no Ivy measurement is reported, only Verus's own two proofs of the lock.
• Performance evidence is thin. IronKV ran as three servers and a 10-thread client on one laptop with payloads capped at 512 bytes (100 trials per bar, with confidence intervals). The log benchmark does not say how many threads append, so the lock explanation for parity is plausible but untested. Verus-mimalloc is slower on six of the eight benchmarks it completes (sh6benchN takes 2.0 s against 0.14 s, glibc-simple 6.6 s against 1.2 s) and ties only on the two cache-scratch runs. The paper does not say what causes the gap, only that a subset of mimalloc's features and optimizations is implemented, so no profile ties the slowdown to the missing ones.
• Usability is claimed, not studied. The goal of reaching developers without deep verification expertise is not tested: the five case studies were built by the authors, who also develop Verus, and outside use is only listed (cluster controllers, a microkernel, a confidential-VM module, LLM-produced code). The VerusSync metatheory is stated ("our metatheory shows") with no proof or citation in the paper.

• Automating the EPR boilerplate, which the authors name as a Verus need, so that small protocols like the lock benefit too.
• Finishing the allocator (realloc, aligned and large allocations) and closing its performance gap, with a profile of where the time goes.
• Measuring effort and expertise directly: person-hours, defects caught in the production log, and a study with developers outside the Verus group, since the paper's broader-community goal depends on it.
• Verifying larger systems on Verus, the authors' stated frontier, and finding abstractions that lower the page table's ratio. Atmosphere is a later example of a microkernel verified with Verus.