Verus overview
Getting started
1.
Getting started
Tutorial
2.
Basic specifications
2.1.
assert, requires, ensures, ghost code
2.2.
Expressions and operators for specifications
2.3.
Integers and arithmetic
2.4.
Equality
3.
Specification code, proof code, executable code
3.1.
spec functions
3.2.
proof functions, proof blocks, assert-by
3.3.
spec functions vs. proof functions, recommends
3.4.
Ghost code vs. exec code
3.5.
const declarations
4.
Recursion and loops
4.1.
Recursive spec functions, decreases, fuel
4.2.
Recursive exec and proof functions, proofs by induction
4.3.
Loops and invariants
4.3.1.
Loops with break
4.4.
Lexicographic decreases clauses and mutual recursion
5.
Datatypes: struct and enum
5.1.
Defining datatypes
5.2.
Querying the discriminant (#[is_variant])
5.3.
Proving properties of fields
6.
Basic libraries and spec closures
6.1.
Specification libraries: Seq, Set, Map
6.2.
INTERLUDE: using assert and assume to develop proofs
6.3.
Spec closures
6.4.
Executable libraries: Vec
7.
Quantifiers
7.1.
forall and triggers
7.2.
Multiple variables, multiple triggers, matching loops
7.3.
exists and choose
7.4.
Proofs about forall and exists
7.5.
Example: binary search
7.6.
Ambient (broadcast) lemmas
8.
Higher-order executable functions
8.1.
Passing functions as values
8.2.
Closures
9.
SMT solving, automation, and where automation fails
9.1.
What's decidable, what's undecidable, what's fast, what's slow
9.2.
Integers and nonlinear arithmetic
9.3.
Bit vectors and bitwise operations
9.4.
forall and exists: writing and using triggers, inline functions
9.5.
Recursive functions
9.6.
Extensional equality
9.7.
Libraries: incomplete axioms for Seq, Set, Map
10.
Improving SMT performance
10.1.
Modules, hiding, opaque, reveal
10.2.
Quantifier profiling
10.3.
Hiding local proofs with assert (...) by { ... }
10.4.
Structured proof by calculation
10.5.
Proof by computation
10.6.
Spinning off separate SMT queries
10.7.
Breaking proofs into smaller pieces
11.
Mutation, references, and borrowing
11.1.
Requires and ensures with mutable references
11.2.
Assertions containing mutable references
12.
Traits
13.
Ghost and tracked variables
14.
Concurrency and Unsafe Code
15.
Attributes and directives
15.1.
external and external_body
15.2.
inline
15.3.
opaque
15.4.
decreases_by
15.5.
when_used_as_spec
16.
Strings
16.1.
String library
16.2.
String literals
17.
Macros
18.
Tools and command-line options
18.1.
Proof Debugger
18.2.
IDE Support
18.3.
Syntax Highlighting
19.
Verification and Rust
19.1.
Why Rust?
19.2.
Supported Rust features
19.3.
Borrowing and lifetimes
19.4.
Mutable borrows
19.5.
Interior mutability
19.6.
Alternatives to unsafe
20.
Understanding the guarantees of a verified program
20.1.
Assumptions and trusted components
20.2.
Identifying a project's TCB
20.3.
Memory safety is conditional on verification
21.
Project setup and development
21.1.
Working with crates
21.2.
Invoking Verus code from Rust
21.3.
Documentation with Rustdoc
Reference
22.
Supported and unsupported Rust features
23.
Verus syntax overview
24.
Modes
24.1.
Function modes
24.2.
Variable modes
25.
Spec expressions
25.1.
Rust subset
25.2.
Arithmetic
25.3.
Spec equality (==)
25.4.
Extensional equality (=~=, =~~=)
25.5.
Prefix and/or (&&& and |||)
25.6.
Chained operators
25.7.
Implication (==>, <==, and <==>)
25.8.
Quantifiers (forall, exists)
25.9.
Such that (choose)
25.10.
Function expressions
25.11.
Trigger annotations
25.12.
The view function @
25.13.
Spec index operator []
26.
Proof features
26.1.
assert and assume
26.2.
assert ... by
26.3.
assert forall ... by
26.4.
assert ... by(bit_vector)
26.5.
assert ... by(nonlinear_arith)
26.6.
assert ... by(compute) / by(compute_only)
26.7.
reveal
26.8.
fuel
27.
Function specifications
27.1.
requires / ensures
27.2.
opens_invariants
27.3.
recommends
28.
Loop specifications
28.1.
invariant
28.2.
invariant_except_break / ensures
29.
Recursion and termination
29.1.
decreases ...
29.2.
decreases ... when ...
29.3.
decreases ... via ...
29.4.
Datatype ordering
29.5.
Cyclic definitions
30.
Misc. Rust features
30.1.
Statics
30.2.
char
31.
Command line
31.1.
--record
32.
Planned future work
Light (default)
Rust
Coal
Navy
Ayu
Verus Tutorial and Reference
Such that (
choose
)
The such-that operator (
choose
) is explained in
exists and choose
.