Verus overview
Getting started
1.
Getting started
1.1.
... on the command line
1.2.
... with VSCode
Tutorial: Fundamentals
2.
Using Verus within Rust
3.
Basic specifications
3.1.
assert, requires, ensures, ghost code
3.2.
Expressions and operators for specifications
3.3.
Integers and arithmetic
3.4.
Equality
4.
Specification code, proof code, executable code
4.1.
spec functions
4.2.
proof functions, proof blocks, assert-by
4.3.
spec functions vs. proof functions, recommends
4.4.
Ghost code vs. exec code
4.5.
const declarations
4.6.
Putting it all together
5.
Recursion and loops
5.1.
Recursive spec functions, decreases, fuel
5.2.
Recursive exec and proof functions, proofs by induction
5.2.1.
Lightweight termination checking
5.3.
Loops and invariants
5.3.1.
Loops with break
5.3.2.
For Loops
5.4.
Lexicographic decreases clauses and mutual recursion
6.
Datatypes: struct and enum
6.1.
Struct
6.2.
Enum
7.
Libraries
7.1.
Specification libraries: Seq, Set, Map
7.2.
Executable libraries: Vec
8.
Spec closures
Tutorial: Understanding the prover
9.
Developing proofs
9.1.
Using assert and assume
9.2.
Devising loop invariants
9.3.
Proving absence of overflow
10.
Quantifiers
10.1.
forall and triggers
10.2.
Multiple variables, multiple triggers, matching loops
10.3.
exists and choose
10.4.
Proofs about forall and exists
10.5.
Example: binary search
10.6.
Ambient (broadcast) lemmas
11.
SMT solving, automation, and where automation fails
11.1.
What's decidable, what's undecidable, what's fast, what's slow
11.2.
Integers and nonlinear arithmetic
11.3.
Bit vectors and bitwise operations
11.4.
forall and exists: writing and using triggers, inline functions
11.5.
Recursive functions
11.6.
Extensional equality
11.7.
Libraries: incomplete axioms for Seq, Set, Map
12.
Managing proof performance and why it's critical
12.1.
Measuring verification performance
12.2.
Quantifier profiling
12.3.
Modules, hiding, opaque, reveal
12.4.
Hiding local proofs with assert (...) by { ... }
12.5.
Structured proofs by calculation
12.6.
Proof by computation
12.7.
Spinning off separate SMT queries
12.8.
Breaking proofs into smaller pieces
13.
Checklist: what to do when proofs go wrong
Tutorial: Verification and Rust
14.
Mutation, references, and borrowing
14.1.
Requires and ensures with mutable references
14.2.
Assertions about mutable references
15.
Traits
16.
Higher-order executable functions
16.1.
Passing functions as values
16.2.
Closures
17.
Ghost and tracked variables
18.
Strings
19.
Macros
20.
Unsafe code & complex ownership
20.1.
Cells / interior mutability
20.2.
Pointers
20.3.
Concurrency
21.
Verifying a container library: Binary Search Tree
21.1.
First draft
21.2.
Encapsulating well-formedness with type invariants
21.3.
Making it generic
21.4.
Implementing Clone
21.5.
Full source for the examples
22.
Interacting with unverified code
22.1.
Calling unverified code from verified code
22.2.
Calling verified code from unverified code
23.
Understanding the guarantees of a verified program
23.1.
Assumptions and trusted components
23.2.
Memory safety is conditional on verification
23.3.
Calling verified code from unverified code
Installation, configuration, and tooling
24.
Installation and setup
24.1.
IDE Support
24.2.
Installing and configuring Singular
25.
Project setup and development
25.1.
Working with crates
25.2.
Invoking Verus code from Rust
25.3.
Documentation with Rustdoc
Reference
26.
Supported and unsupported Rust features
27.
Verus syntax by example
28.
Modes
28.1.
Function modes
28.2.
Variable modes
29.
Contributed Extensions
29.1.
Automatic spec to exec functions
29.2.
Spec and proof attributes for exec functions
29.2.1.
Automatic exec to spec functions
30.
Spec expressions
30.1.
Rust subset
30.2.
Operator Precedence
30.3.
Arithmetic
30.4.
Bit operators
30.5.
Coercion with as
30.6.
Spec equality (==)
30.7.
Extensional equality (=~=, =~~=)
30.8.
Prefix and/or (&&& and |||)
30.9.
Chained operators
30.10.
Implication (==>, <==, and <==>)
30.11.
Quantifiers (forall, exists)
30.12.
Such that (choose)
30.13.
Trigger annotations
30.14.
The view function @
30.15.
Spec index operator []
30.16.
decreases_to!
31.
Proof features
31.1.
assert and assume
31.2.
assert ... by
31.3.
assert forall ... by
31.4.
assert ... by(bit_vector)
31.5.
assert ... by(nonlinear_arith)
31.6.
assert ... by(compute) / by(compute_only)
31.7.
reveal, reveal_with_fuel, hide
32.
Function specifications
32.1.
Function Signatures
32.1.1.
Exec fn signature
32.1.2.
Proof fn signature
32.1.3.
Spec fn signature
32.2.
Signature clauses
32.2.1.
requires / ensures
32.2.2.
returns
32.2.3.
opens_invariants
32.2.4.
no_unwind
32.2.5.
recommends
32.3.
Traits and signature inheritance
32.4.
Specifications on FnOnce
33.
Loop specifications
33.1.
invariant
33.2.
invariant_except_break / ensures
34.
Recursion and termination
34.1.
decreases ... when ... via ...
34.2.
Datatype ordering
34.3.
Cyclic definitions
35.
Type invariants
36.
Attribute list
37.
Directives
37.1.
assume_specification
37.2.
global
38.
Misc. Rust features
38.1.
Statics
38.2.
char
38.3.
Unions
38.4.
Pointers and cells
39.
Command line
39.1.
--record
40.
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
.