Full Verus clone with pure-Rust z4 SMT backend. v1.0: 100% feature parity (29/29 Verus features). No Z3. No C. No FFI.

Author: Andrew Yates andrewyates.name@gmail.com · Version: 1.0.0 · License: Apache-2.0 Copyright: 2026 Dropbox

Certus lets you write mathematical proofs about Rust code using annotations — preconditions, postconditions, loop invariants, termination measures, quantifiers — and verifies them automatically using the z4 SMT solver. It is a complete Verus replacement built entirely in Rust.

use certus::*;

#[certus::proof]
fn lemma_double_positive(x: u64) {
    certus::requires!(x > 0);
    certus::ensures!(x + x > x);
    // z4 proves: for all x > 0, x + x > x (under bitvector arithmetic)
}

#[certus::proof]
#[certus::decreases(n)]
fn lemma_sum_nonneg(n: u64) {
    if n > 0 {
        lemma_sum_nonneg(n - 1);  // recursive example; self-recursion verified via fuel encoding
    }
    certus::assert!(sum(n) >= 0);
}

When you run cargo test, certus collects proof obligations from your annotations and sends them to z4. Each assertion is checked via refutation: z4 attempts to find a counterexample to NOT(assertion). If no counterexample exists (UNSAT), the assertion is verified. If z4 finds one, it reports the concrete values that violate the property.

crates/
├── cargo-certus/         # CLI wrapper (`cargo certus check`)
├── certus/               # Proc macros (#[proof], #[decreases], requires!, etc.)
├── certus-core/          # Verification engine (encoder, VC generation, z4 interface)
├── certus-types/         # Ghost types (Seq, Set, Map) for specifications
├── certus-merge-contract/# Versioned MergeBundle boundary for zani integration
└── certus-merge-runner/  # Merge parity gate runner

Annotated Rust code
    │
    ▼
Proc macros expand annotations        (certus/src/lib.rs)
    │
    ▼
Obligation collection via              (certus-core/src/verify_macro.rs)
thread-local context
    │
    ▼
Rust expressions lowered to CertusExpr (certus-core/src/ir_lowering/)
typed IR and encoded to z4 terms
    │
    ▼
Z4Encoder encodes obligations:         (certus-core/src/encoder/)
  - Declare variables with correct
    sorts (i32→BV32, u64→BV64, etc.)
  - Add assumptions as constraints
  - For each assertion: check SAT(¬P)
    │
    ├─ UNSAT  → Verified ✓
    ├─ SAT    → Counterexample (model extracted)
    └─ Unknown → solver limit reached

Each proc macro generates code for three cfg targets:

The encoder (encoder/) handles:

• Bitvector arithmetic — i8/u8 through i128/u128 with correct width and signedness
• Boolean logic — &&, ||, !, with proper short-circuit semantics
• Comparisons — signed and unsigned variants selected per-expression
• Type casts — widening (sign/zero extend), narrowing (extract), signed↔unsigned
• Collections — Seq<T> as Array(BV64, T), Set<T> as Array(T, Bool), Map<K,V> as Array(K, V)
• Quantifiers — forall! and exists! with trigger patterns
• Match expressions — compiled to chained if-then-else
• Function calls — recursive functions as uninterpreted functions with decrease checks
• Division safety — literal division by zero rejected during encoding; variable divisors checked via SMT

Solver limits: 30s timeout / 128MB term-memory per assertion (overridable via #[rlimit]). BV-mode queries use a 10s thread watchdog since z4-dpll's BV solver bypasses internal timeout. Extended retry uses 20s for marginal BV timeouts (#2313).

The in-tree performance proof and regression-gate coverage is maintained in the internal engineering notes that are not shipped in the public mirror.

The tables below highlight the common user-facing surface. The fuller exported proc-macro inventory lives in crates/certus/src/lib.rs.

Feature-gated behind tla2. This bridge remains in certus for compatibility and internal experiments, but protocol verification is not part of the active certus roadmap; strategic ownership lives in zani / tRust.

Specification-only collection types. These are PhantomData wrappers — zero runtime cost, used only in proof context.

Build: Passes. Tests: 5,800+ pass, 0 fail. Verus parity: 100% (29/29 features). Lines: 244k Rust across 6 crates.

• Full proc macro suite (59 macros) with three-way cfg expansion (test/zani/runtime)
• End-to-end verification: annotation → obligation collection → z4 solving → result
• Bitvector-precise arithmetic for all Rust integer types (i8–i128, u8–u128)
• Pre/postconditions, loop invariants, proof functions, recursive termination (self + mutual via Tarjan SCC)
• Quantifiers (forall/exists) with automatic trigger inference
• Ghost collections (Seq, Set, Map, Multiset) with higher-order combinators (fold, filter, map, flat_map)
• Datatype encoding (Option/Result, recursive ADTs), polymorphism (Poly/Box/Unbox), trait verification
• Mutable reference verification via SSA shadow rewriting
• Place-based reasoning for memory locations
• Mode-aware overflow/division/shift checking (OverflowBehavior/Div0Behavior/BitshiftBehavior)
• Real number arithmetic, nondeterministic expressions, prophecy variables
• Broadcast lemmas, reveal/hide/opaque, inline spec functions, SMT pruning
• calc!, assert_by, assert_by_contradiction, assert_by_compute, choose
• Proof-call postcondition propagation (ensures assumed at call site)
• Loop invariant auto-inference for for i in range loops
• Per-function rlimit, recommends clauses, extern specs
• Specialized solver modes: nonlinear arithmetic, bitvector, compute
• SMT reachability pruning to reduce solver load
• Compile-fail tests via trybuild, 300+ integration test files

• zani integration — certus ships MergeBundle v4, waiting on zani consumer (#1994)

Certus will merge into zani alongside sunder to form a unified Rust verification tool:

certus (Verus-style proofs) ──┐
                              ├──► zani (unified) ──► tRust
sunder (separation logic) ────┘

Current merge staging:

1. certus exports a versioned MergeBundle boundary via certus-merge-contract.
2. zani must add a production consumer for that bundle and pass parity coverage through that ingest path.
3. Only after that ingest/parity gate exists can certus crates relocate into zani.

cargo build
cargo test

The cargo-fuzz suite for contradictory postconditions lives under fuzz/ and exercises the VC extraction plus encoder path.

cargo test --manifest-path fuzz/Cargo.toml

For a 1-hour release sweep, run each target for 15 minutes:

cargo fuzz run ensures_false -- -max_total_time=900
cargo fuzz run strict_inequality -- -max_total_time=900
cargo fuzz run mode_crossing -- -max_total_time=900
cargo fuzz run collections_contradiction -- -max_total_time=900

Extended fuzzing runbooks stay in the internal development docs; the public mirror keeps the executable fuzz targets and commands above.

The public mirror ships the crate sources, examples, and tests. The broader engineering deep dives stay in the private development repo. Those internal notes cover:

• Verus parity tracking and follow-on roadmap
• Unsigned overflow semantics
• z4 backend architecture
• Verification idioms and proof patterns
• Termination encoding and #[decreases] semantics
• Rust-to-z4 type mapping
• __certus_* metadata for zani integration

Apache 2.0. Copyright 2026 Dropbox