Certora Verification Language for Rust (CVLR)

CVLR stands for Certora Verification Language for Rust. It is pronounced like “cavalier”. CVLR provides the basic primitives for writing verification rules that specify pre- and post-conditions for client code. Unlike CVL for Solidity, CVLR is embedded in Rust. It is compiled by the Rust compiler and has simple operational semantics.

CVLR is deployed to crates.io. The development version can be found at https://github.com/Certora/cvlr. CVLR is independent of the Solana ecosystem; Solana-specific helpers live in cvlr-solana.

Note

This page documents the language at a high level. For end-to-end patterns (account harnesses, mocks, parametric rules, methodology) see the dedicated pages listed in the Contents of this section.

The cvlr::prelude

The recommended import for spec files is:

use cvlr::prelude::*;

The prelude pulls in the items you almost always need:

From the prelude

What it is

rule

the #[rule] attribute

nondet

the nondet::<T>() function

cvlr_assert!

assertion macro

cvlr_assert_{eq,ne,le,lt,ge,gt}!

comparison-aware assertions (log both sides)

cvlr_assert_that! / cvlr_assert_all!

the assertion DSL — see cvlr_assert_that! — comparison-aware DSL

cvlr_assume!

restrict the search space (precondition)

cvlr_assume_{eq,ne,le,lt,ge,gt}!

matching specialized assume variants

cvlr_assume_that! / cvlr_assume_all!

the assume DSL

cvlr_satisfy!

existential check (at least one execution …)

clog!

log values into counterexamples

Nondet, CvlrLog

derive macros (from cvlr::derive)

Individual items can also be imported directly (e.g. use cvlr::{rule, nondet};).

CVLR Rules

Specifications are written as pre- and post-conditions in rules. A rule is similar to a unit test. However, instead of being executed for some specific input, the rule is symbolically analyzed for all possible non-deterministic values.

In CVLR, rules are regular Rust functions, annotated with #[rule].

A complete example of a specification with several rules is shown below. The function being verified is compute_fee. We have included it in the spec file for simplicity.

use cvlr::prelude::*;

pub fn compute_fee(amount: u64, fee_bps: u16) -> Option<u64> {
    if amount == 0 { return None; }
    let fee = amount.checked_mul(fee_bps).checked_div(10_000);
    fee
}

#[rule]
pub fn rule_fee_sanity() {
   compute_fee(nondet(), nondet()).unwrap();
   cvlr_satisfy!(true);
}

#[rule]
pub fn rule_fee_assessed() {
    let amt: u64 = nondet();
    let fee_bps: u16 = nondet();
    cvlr_assume!(fee_bps <= 10_000);
    let fee = compute_fee(amt, fee_bps).unwrap();
    clog!(amt, fee_bps, fee);
    cvlr_assert!(fee <= amt);
    if fee_bps > 0 { cvlr_assert!(fee > 0); }
}

#[rule]
pub fn rule_fee_liveness() {
    let amt: u64 = nondet();
    let fee_bps: u16 = nondet();
    cvlr_assume!(fee_bps <= 10_000);
    let fee = compute_fee(amt, fee_bps);
    clog!(amt, fee_bps, fee);
    if fee.is_none() { cvlr_assert!(amt == 0); }
}

The rule rule_fee_sanity checks that the function under verification has at least one panic-free execution. A rule like that is called a sanity rule. It is a good practice to start a specification with such a rule.

The rule rule_fee_assessed checks that a fee can be computed for an arbitrary amount. It has two assertions. The first checks that the fee is never greater than the amount. The second checks that the fee is always assessed when required. The first assertion is not violated. However, the second is. Can you spot the bug? Note that we have also added calls to the log macro clog! that is similar to the dbg! macro in Rust. The clog! macro will instruct the Prover to produce the values of the desired variables in any violating execution.

The rule rule_fee_liveness checks that the fee is always computed, except when the fee rate is 0. This assertion is violated. Can you spot the bug?

Assertions

The simplest feature of CVLR is assertions. An assertion is written as cvlr_assert!(cond), where cond is the condition being asserted. The semantics is the same as traditional asserts in Rust — an assertion is violated if there is (a panic-free) execution that reaches cvlr_assert!(cond) and in the current execution state cond is false.

For example, cvlr_assert!(true) is never violated, while cvlr_assert!(false) is always violated when reached.

What makes cvlr_assert! special is that it is verified symbolically by the Certora Prover. That is, the Prover returns Violated if there is an input and an execution of the program that reaches that assertion and violates it.

Assertion variants

All assertion macros come from cvlr::prelude::*. They desugar to the same thing: a check that fails the rule when the condition is false. The specialized forms produce better counterexample messages because they report both sides of the comparison.

Macro

Use for

Equivalent to

cvlr_assert!(cond)

a single boolean condition

the canonical form

cvlr_assert_eq!(a, b)

equality

cvlr_assert!(a == b) with better messages

cvlr_assert_ne!(a, b)

inequality

cvlr_assert!(a != b)

cvlr_assert_lt!(a, b)

strict less-than

cvlr_assert!(a < b)

cvlr_assert_le!(a, b)

less-or-equal

cvlr_assert!(a <= b)

cvlr_assert_gt!(a, b)

strict greater-than

cvlr_assert!(a > b)

cvlr_assert_ge!(a, b)

greater-or-equal

cvlr_assert!(a >= b)

The assume macros mirror the assertion family one-for-one: cvlr_assume_eq!, cvlr_assume_ne!, cvlr_assume_le!, cvlr_assume_lt!, cvlr_assume_ge!, cvlr_assume_gt! — same comparisons, but constrain the search space instead of failing the rule.

use cvlr::prelude::*;

#[rule]
pub fn rule_assert_basics() {
    let x: u64 = nondet();
    let y: u64 = nondet();
    cvlr_assume_le!(x, 100);
    cvlr_assume_le!(y, 100);

    cvlr_assert!(x + y >= x);
    cvlr_assert_eq!(x.saturating_sub(y) + y, x.max(y));
    cvlr_assert_le!(x.min(y), x);
    cvlr_assert_lt!(x.saturating_sub(101), 1);
}

Guarded assertions: cvlr_assert_if! and friends

cvlr_assert_if!(guard, body) only fires when guard evaluates to true — useful when the property only makes sense in some branch:

cvlr_assert_if!(amount > 0, fee > 0);

The full guarded family follows the same _eq / _le / _lt / _ge / _gt / _ne suffixes: cvlr_assert_eq_if!(guard, a, b), cvlr_assert_le_if!(guard, a, b), and so on.

cvlr_assert_that! — comparison-aware DSL

cvlr_assert_that!(expr) looks at expr and picks the most informative underlying macro automatically:

cvlr_assert_that!(a < b);          // -> cvlr_assert_lt!(a, b)
cvlr_assert_that!(a == b);         // -> cvlr_assert_eq!(a, b)
cvlr_assert_that!(p && q);         // -> cvlr_assert!(p && q)
cvlr_assert_that!(if cond { a > b });   // guarded form

Use it when you’d rather write the condition once than juggle suffixes. The matching cvlr_assume_that! does the same lowering for assumes, and cvlr_eval_that! evaluates without asserting (useful when you need the bool back).

Bulk assertions: cvlr_assert_all!

cvlr_assert_all! takes a list of conditions and asserts each in turn — each becomes its own underlying assertion, so the counterexample identifies which conjunct failed:

cvlr_assert_all!(
    post.tokens >= pre.tokens,
    post.shares <= post.tokens,
    post.tokens < cap
);

cvlr_assume_all! is the corresponding bulk assume. cvlr_eval_all! returns a single bool that is the AND of all the conjuncts.

cvlr_satisfy! — existential checks

Often, the intended meaning of an assertion is that it should not be violated, i.e., to hold on all possible executions. However, sometimes it is useful to check whether some execution is possible. In that case, the specification intends for the assertion to be reachable. For such cases, CVLR provides a satisfy assertion, called cvlr_satisfy!(cond).

The semantics of cvlr_satisfy!(cond) is that it is Violated when it is either not reached, or when every execution that reaches it violates the condition. For example, cvlr_satisfy!(true) is violated only if it is never reachable (i.e., part of dead code), and cvlr_satisfy!(false) is always violated.

#[rule]
pub fn rule_zero_is_reachable() {
    let x: u64 = nondet();
    cvlr_assume!(x < 10);
    cvlr_satisfy!(x == 0);              // passes: x = 0 is reachable
}

Inside a rule that contains cvlr_satisfy!, ordinary cvlr_assert!s become additional constraints (treated like assumes). This means you can write rules of the form “is there an execution that reaches X without violating Y?”.

Typical uses:

  • Reachability of a code path (cvlr_satisfy!(reached_branch)).

  • “Liveness” sanity: “the protocol can move from state A to state B”.

Assumptions

Assumptions provide a way to restrict input to reflect some pre-condition. CVLR provides an assumption macro cvlr_assume!(cond). If an execution reaches cvlr_assume!(cond), it continues only if cond is true in the current program state. Otherwise, the execution aborts.

For example, cvlr_assume!(true) is a noop, while cvlr_assume!(false) blocks all executions that reach it.

A typical use of cvlr_assume! is to restrict a range of a value beyond the restriction afforded by its type. For example, restricting the maximum value of a variable to 100 can be done as follows:

let fee_bps = get_some_fee();
cvlr_assume!(fee_bps <= 100)
// computation reaches here only if fee_bps is no greater than 100

cvlr_assume! is the right tool when:

  • You need a precondition (amount > 0).

  • You’re encoding an invariant the rest of the system maintains (shares <= tokens).

  • You want to filter to the slice of state that is interesting for a given rule.

It is the wrong tool when:

  • You’re trying to silence a counterexample. If a counterexample is real, the property is wrong; tightening the assume hides bugs.

  • You want a property to hold “in practice”. Either prove it, or document the precondition and prove it separately.

Warning

Watch out for vacuity. Two contradicting assumes (x > 10 and x < 5) make every assertion trivially “pass”. The Prover’s vacuity check (enabled via "rule_sanity": "basic") catches this — see Vacuity checks.

Nondeterministic Values

A specification must tell the Prover what are the (symbolic) inputs that the Prover has to explore. Such values are called non-deterministic. The name comes from the fact that the Prover chooses the values non-deterministically (i.e., not following any specific pre-determined exploration scheme or probability distribution). Nondet values are similar to arbitrary values in property-based testing, except that they are not chosen randomly, but are explored exhaustively via symbolic reasoning.

CVLR provides a generic function nondet() that can generate non-deterministic values of all primitive integers. For example, nondet::<u64>() returns a non-deterministic u64, and nondet::<u16>() returns a non-deterministic u16.

let x: u64   = nondet();
let b: bool  = nondet();
let v: i32   = nondet::<i32>();        // turbofish if no type context
let arr: [u8; 32] = nondet();

Every call returns a fresh, independent havoced value. The Prover treats them as universally quantified: any execution that demonstrates a property violation, for any combination of these values, is a counterexample.

For non-primitive types and Solana-specific helpers (Pubkey, AccountInfo, bounded vectors, …) see Nondet & Havoc.

Logging with clog!

clog! writes values into the counterexample report. It is a no-op when the rule passes; there is no cost to leaving it in production specs.

clog!();                       // position marker (no values logged)
clog!(amount);                 // single primitive
clog!(x, y, r);                // multiple primitives in one call
clog!(pre, post);              // structs implementing CvlrLog

Tip

Rule of thumb: every value you produced with nondet() should appear in some clog! before any assertion that depends on it. A counterexample without logged inputs is hard to read.

CvlrLog — log your own structs

To clog! a custom struct, derive CvlrLog (shipped with cvlr ≥ 0.5):

use cvlr::prelude::*;

#[derive(cvlr::derive::CvlrLog)]
pub struct VaultSnapshot {
    pub tokens: u64,
    pub shares: u64,
}

let pre  = VaultSnapshot { tokens: vault.tokens, shares: vault.shares };
// ... run handler ...
let post = VaultSnapshot { tokens: vault.tokens, shares: vault.shares };
clog!(pre, post);
cvlr_assert_le!(post.shares, post.tokens);

Counterexamples will then show both snapshots with all named fields. The derive works on structs (named or tuple) and on enums (each variant is logged with its field values).

Manual impl CvlrLog

Reach for the manual impl only when you want a custom layout — for example, omitting some fields, renaming them in the report, or logging a derived value:

use cvlr::log::{cvlr_log_with, CvlrLog, CvlrLogger};

impl CvlrLog for VaultSnapshot {
    #[inline(always)]
    fn log(&self, tag: &str, logger: &mut CvlrLogger) {
        logger.log_scope_start(tag);
        cvlr_log_with("tokens", &self.tokens, logger);
        cvlr_log_with("shares", &self.shares, logger);
        logger.log_scope_end(tag);
    }
}

mathint::NativeInt — arithmetic without overflow noise

When you write cvlr_assert!(post.tokens >= pre.tokens), you mean it mathematically — but the Prover sees u64 arithmetic with wraparound. Tiny overflow corner cases will then become spurious counterexamples.

cvlr::mathint::NativeInt is an unbounded integer that the Prover treats as mathematical. Convert at the boundary, do arithmetic in NativeInt, and optionally re-bound at the end.

use cvlr::mathint::NativeInt;
use cvlr::prelude::*;

#[rule]
pub fn rule_no_dilution() {
    let pre_tokens: u64  = nondet();
    let pre_shares: u64  = nondet();
    let amount:     u64  = nondet();

    // Lift into NativeInt for safe arithmetic.
    let t: NativeInt = pre_tokens.into();
    let s: NativeInt = pre_shares.into();
    let a: NativeInt = amount.into();

    // Express the precondition mathematically.
    cvlr_assume!(s <= t);

    // Constrain to the representable range when needed.
    let new_tokens = t + a;
    cvlr_assume!(NativeInt::is_u64(new_tokens));

    // The property: new ratio is no worse than the old one.
    cvlr_assert!(s * new_tokens <= (s + a) * t);
}

Useful operations on NativeInt:

Method

Purpose

NativeInt::from(x: u64)

lift a u64

n.into() : NativeInt

(same, via Into)

NativeInt::is_u64(n)

true if n fits in u64

NativeInt::is_u128(n)

true if n fits in u128

+, -, *, comparison

unbounded arithmetic

Use NativeInt for solvency / monotonicity invariants where overflow would only be a real bug if it could actually happen. Don’t reach for it when u64 is genuinely the right model (e.g. simulating a counter that wraps).

Putting it together

The shape of most practical specs is: snapshot the pre-state, restrict it with assume_pre, run the handler, snapshot the post-state, log both, and assert a relation:

use cvlr::mathint::NativeInt;
use cvlr::prelude::*;

// Snapshot type with a CvlrLog impl as shown in the previous section
// (substituting NativeInt for the field types).
pub struct Snapshot { tokens: NativeInt, shares: NativeInt }
// impl CvlrLog for Snapshot { /* … as above … */ }

#[rule]
pub fn rule_deposit_preserves_solvency() {
    let mut tokens: u64 = nondet();
    let mut shares: u64 = nondet();
    let pre = Snapshot { tokens: tokens.into(), shares: shares.into() };
    cvlr_assume!(pre.shares <= pre.tokens);

    let amount: u64 = nondet();
    cvlr_assume!(NativeInt::is_u64(pre.tokens + NativeInt::from(amount)));
    tokens = (pre.tokens + NativeInt::from(amount)).try_into().unwrap();
    shares = nondet();

    let post = Snapshot { tokens: tokens.into(), shares: shares.into() };
    clog!(pre, post);
    cvlr_assume!(post.shares <= post.tokens);
    cvlr_assert_le!(post.shares, post.tokens);
}

This pre / assume_pre / run / post / clog! / assert sequence is the standard shape of practical specs. It is generalized in Parametric Rules & Macros.

What’s next