DRAFT

Verus blog

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

Verus is open-source at github.com/verus-lang/verus

Verus Announcements

2024-02-13
Travis Hance

Hi folks, we recently renamed FnSpec to spec_fn. FnSpec was originally named following the convention of FnOnce, etc., but since it's a type rather than a trait, we decided to make it look more like fn instead. Hence, spec_fn.

FnSpec should keep working for the time being, except for the deprecation warnings, but will be removed at some point.
2024-02-13
Jay Lorch

Thanks to Alex Bai and others, Verus now has a standard library for arithmetic, based on Dafny's. You can use it by importing from vstd::arithmetic, e.g., with

use vstd::arithmetic::div_mod::{lemma_fundamental_div_mod, lemma_mod_bound};

Documentation is at this link.
2024-02-12
Andrea Lattuada

Hi all! I have just merged PR 978. Next time you pull main you will need to obtain z3 4.12.5 (using ./tools/get-z3.(sh|ps1). Vargo will check that the current version of z3 is the correct one, and let you know otherwise (you can override this check with --no-solver-version-check but note that current Verus will only successfully build with 4.12.5 (as we are using a new z3 option that was released in this version). As a reminder: updating z3 may cause existing proofs to break (due to changes in z3’s heuristics). Based on preliminary testing we expect limited breakage but be aware that when you pick up the merge commit you may need to tweak the proofs for certain functions. Let us know if you experience extensive breakage or if you encounter other issues.
2024-02-09
Andrea Lattuada

Hi folks! A heads up that I am planning to merge PR 978 on Monday morning UTC. This will upgrade z3 to the latest release (4.12.5); this may cause existing proofs to break (due to changes in z3’s heuristics). Based on preliminary testing we expect limited breakage but be aware that when you pick up the merge commit you may need to tweak the proofs for certain functions. I will post another announcement when I merge the change.
2024-01-31
Travis Hance

Hello, you can now pass named functions directly as values (exec functions only). For example:

fn a<F: Fn(u8) -> bool>(f: F) { ... }

fn b(value: u8) -> bool { ... }


fn main() {
// This now works:
a(b);


// Previously you would have had to create a closure:
a(|x: u8| b(x));
}

As with closures, you can use b.requires(args) and b.ensures(args, output) to access the precondition and postcondition. You can also use call_requires(b, args) or call_ensures(b, args, output).
2024-01-15
Travis Hance

The '?' operator is now supported.
2023-11-07
Chris Hawblitzel

I'm about to merge https://github.com/verus-lang/verus/pull/771 . With this, any items (e.g. functions, datatypes, etc.) declared outside the verus! macro will be considered external to the verifier by default. This means that by default, Verus will not attempt to verify or process such items. If you want such an item to be verified or visible to the verifier, you can either put it inside verus! or mark it #[verifier::verify]. The reason for this new behavior is that some projects contain a lot of unverified code and a little verified code, and we don't want to have to mark every item in the unverified code as #[verifier::external]. (For backwards compatibility, if you don't want this new default behavior, there is for now a flag --no-external-by-default that will opt out of this new behavior and restore the old behavior.)
2023-11-06
Andrea Lattuada

Hi folks! I am about to merge a pull request that replaces --arch-word-bits with a new directive global size_of usize == 8; (or global size_of usize == 4;) which sets the size of usize (and isize, as it's related) and adds a static assertion that, when compiled, usize has the expected size. If you're using --arch-word-bits 64 you'll now need global size_of usize == 8; inside the verus! macro, ideally at the root of your project. This change does not yet support core::mem::size_of::<usize>(), but an upcoming one will.
2023-10-17
Andrea Lattuada

Hi folks! FYI, I pushed a commit that re-organizes the command line options to reduce the number of top-level options, moving some of the less commonly used features to sub-flags, to make --help easier to scan. In particular, there's a new set of options (-V, modeled against rustc's -Z) for extended/experimental flags.
2023-09-21
Andrea Lattuada

Hi folks, I am about to merge two commits that require action from users:

  • next time you pull, please rebuild vargo by following Step 3 of https://github.com/verus-lang/verus/blob/main/INSTALL.md, and
  • assert forall #![trigger Q(x)] |x| P(x) is now consistent with regular forall, i.e. you will need to change those to assert forall |x| #![trigger Q(x)] P(x) (the trigger annotation moves after the |x|). The same applies for #![auto].
2023-09-21
Andrea Lattuada

At the moment, you may need to run vargo clean -p vstd --release before rebuilding Verus (if you’re getting an error message about the vstd fingerprint file). (Thank you @Jay Lorch for the help debugging this issue.)
2023-09-05
Andrea Lattuada

I just merged another commit (https://github.com/verus-lang/verus/commit/0f957d69e8c002969b40a8e4aae97d140cd7d367) that requires re-building vargo when you pull new changes. You will need to rebuild vargo by following Step 3 of https://github.com/verus-lang/verus/blob/main/INSTALL.md .
2023-09-01
Andrea Lattuada

A recent commit accidentally introduced an issue that resulted in imprecise spans being reported for error messages (the parts of the source underlined with ^^^^^^ or ------ in an error message) and caused a bad interaction between rust-analyzer (in vscode) and vargo that resulted in the build cache being invalidated more often than necessary, which caused vargo to often rebuild Verus and its dependencies from scratch. This has been fixed in a recent commit https://github.com/verus-lang/verus/commit/3a7b70f2123b144059073e97d27b05aef04f3bf4. If you have already built Verus and you pull the new changes, you will need to rebuild vargo by following Step 3 of https://github.com/verus-lang/verus/blob/main/INSTALL.md .
2023-08-30
Andrea Lattuada

The pull request https://github.com/verus-lang/verus/pull/741 has just been merged. This changes the mechanism for reveal so that type arguments are not required anymore (see the PR for details). This is a breaking change, because, in an impl for type A, Self:: is not supported anymore in the argument to reveal/reveal_with_fuel/hide; you can replace it with A:: in an impl A block, and with <A as Tr>:: in an impl Tr for A block.
2023-08-29
Chris Hawblitzel

The pull request https://github.com/verus-lang/verus/pull/733 has just been merged. If you have already built Verus and you pull the new changes, you will need to rebuild vargo by following Step 3 of https://github.com/verus-lang/verus/blob/main/INSTALL.md .

A Verus overview

Verus is a tool for verifying the correctness of code written in Rust. The main goal is to verify full functional correctness of low-level systems code, building on ideas from existing verification frameworks like Dafny, Boogie, F*, VCC, Prusti, Creusot, Aeneas, Cogent, Coq, and Isabelle/HOL. Verification is static: Verus adds no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable Rust code will always satisfy some user-provided specifications for all possible executions of the code.

13 February 2024
Written by

A gentle introduction to checking code correctness in Verus

I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.

20 February 2024
Written by