Verus attributes for executable code #

The #[verus_spec] attribute macro can help add Verus specifications and proofs to existing executable code without sacrificing readability.

When to use #[verus_spec] instead of the verus! macro #

The default way to write Verus code is by using the verus! macro. However, using verus! to embed specifications and proofs directly in executable code may not always be ideal for production settings. This is particularly true when developers want to integrate verification into an existing Rust project and aim to:

1. Minimize changes to executable code — avoid modifying function APIs to include tracked or ghost arguments, and preserve native Rust syntax for maintainability.
2. Adopt verification incrementally — apply Verus gradually to a large, existing codebase without requiring a full rewrite of the function APIs.
3. Maintain readability — ensure the verified code remains clean and understandable for developers who are not familiar with Verus or want to ignore verification-related annotations.
4. Optimize dependency management — use Verus components (verus_builtin, verus_builtin_macros, and vstd) in a modular way, allowing projects to define custom stub macros and control Verus dependencies via feature flags.

Adding specifications to a function #

Use #[verus_spec(requires ... ensures ...)] to attach a specification to a function signature.

Here is an example:

{{#include ../../../../examples/guide/exec_attr.rs:verus_spec}}

Adding verification hints #

Use #[verus_verify(...)] to provide hints to the verifier to mark a function as external, external_body, spinoff_prover, or specify a different resource limit via rlimit(amount).

In addition, you can create a dual mode (spec + exec) function via the verus_verify(dual_spec) attribute, which will attempt to generate a spec function from an executable function.

Adding proofs inside functions #

When a function has the #[verus_spec(...)] attribute, we can introduce proofs directly inside executable functions using the proof macros described below.

When Rust builds the code (without using Verus), the #[verus_spec(...)] attribute will ensure all proof code is erased.

Simple proof blocks #

Use proof! to add a proof block; this is equivalent to using proof { ... } inside the verus! macro. This implies that ghost/tracked variables defined inside of proof! are local to that proof block and cannot be used in other proof blocks.

Ghost/Tracked variables across proof blocks #

Use proof_decl! when you need to use ghost or tracked variables across different proof blocks. It will allow you to introduce a proof block and declare function-scoped ghost/tracked variables, as shown in this example:

{{#include ../../../../examples/guide/exec_attr.rs:proof}}

Adding ghost/tracked variables to executable function calls #

• #[verus_spec(with ...)]: Adds tracked or ghost variables as parameters or return values in an executable function.

  This generates two versions of the original function:

  • A verified version (with ghost/tracked parameters), used in verified code.
  • An unverified version (with the original signature), callable from unverified code.

• proof_with! Works in combination with verus_spec to pass tracked/ghost variables to a callee.

  When proof_with! precedes a function call, the verified version is used; otherwise, the unverified version is chosen. The unverified version includes a requires false precondition, ensuring that improper use of proof_with! will cause a verification failure when called from verified code.

Here is an example:

{{#include ../../../../examples/guide/exec_attr.rs:proof_with}}

Using a mix of #[verus_spec] and verus! #

The preferred way to use #[verus_spec] and verus! is to use #[verus_spec] for all executable functions, and use verus! for spec/proof functions.

NOTE: The combination of #[verus_spec(with ...)] + proof_with! currently has compatibility issues with executable functions defined in verus! if the functions involved receive or return ghost/tracked variables.

Specifically, proof_with! works with exec functions verified via #[verus_spec]. Using proof_with! to pass ghost/tracked variables to an exec function verified via verus! will result in this error:

[E0425]: cannot find function `_VERUS_VERIFIED_xxx` in this scope.

This is because verus! always requires a real change to the function's signature and has a single function definition, while #[verus_spec] expects a verified and an unverified version of the function.

To use a function verified by verus!, a workaround is to create a trusted wrapper function and then use it.

#[verus_verify(external_body)]
#[verus_spec(v =>
   with Tracked(perm): Tracked<&mut PointsTo<T>>
   requires
        old(perm).ptr() == ptr,
        old(perm).is_init(),
    ensures
        perm.ptr() == ptr,
        perm.is_uninit(),
        v == old(perm).value(),
)]
fn ptr_mut_read<'a, T>(ptr: *const T)  -> T
{
   vstd::raw_ptr::ptr_mut_read(ptr, Tracked::assume_new())
}

More examples and tests #

{{#include ../../../../examples/syntax_attr.rs}}

{{#include ../../../../source/rust_verify_test/tests/syntax_attr.rs}}