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
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.
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.
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.
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.
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)
.
The '?' operator is now supported.
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.)
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.
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.
Hi folks, I am about to merge two commits that require action from users:
vargo
by following Step 3 of https://github.com/verus-lang/verus/blob/main/INSTALL.md, andassert 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]
.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.)
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 .
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 .
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.
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 .