Verus overview
Getting started
1.
Getting started
Tutorial: Fundamentals
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
3.6.
Putting it all together
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.3.2.
For Loops
4.4.
Lexicographic decreases clauses and mutual recursion
5.
Datatypes: struct and enum
5.1.
Struct
5.2.
Enum
6.
Libraries
6.1.
Specification libraries: Seq, Set, Map
6.2.
Executable libraries: Vec
7.
Spec closures
Tutorial: Understanding the prover
8.
Developing proofs
8.1.
Using assert and assume
8.2.
Devising loop invariants
8.3.
Proving absence of overflow
9.
Quantifiers
9.1.
forall and triggers
9.2.
Multiple variables, multiple triggers, matching loops
9.3.
exists and choose
9.4.
Proofs about forall and exists
9.5.
Example: binary search
9.6.
Ambient (broadcast) lemmas
10.
SMT solving, automation, and where automation fails
10.1.
What's decidable, what's undecidable, what's fast, what's slow
10.2.
Integers and nonlinear arithmetic
10.3.
Bit vectors and bitwise operations
10.4.
forall and exists: writing and using triggers, inline functions
10.5.
Recursive functions
10.6.
Extensional equality
10.7.
Libraries: incomplete axioms for Seq, Set, Map
11.
Managing proof performance and why it's critical
11.1.
Measuring verification performance
11.2.
Quantifier profiling
11.3.
Modules, hiding, opaque, reveal
11.4.
Hiding local proofs with assert (...) by { ... }
11.5.
Structured proof by calculation
11.6.
Proof by computation
11.7.
Spinning off separate SMT queries
11.8.
Breaking proofs into smaller pieces
12.
Checklist: what to do when proofs go wrong
Tutorial: Verification and Rust
13.
Mutation, references, and borrowing
13.1.
Requires and ensures with mutable references
13.2.
Assertions containing mutable references
14.
Traits
15.
Higher-order executable functions
15.1.
Passing functions as values
15.2.
Closures
16.
Ghost and tracked variables
17.
Strings
17.1.
String library
17.2.
String literals
18.
Macros
19.
Unsafe code & complex ownership
19.1.
Cells / interior mutability
19.2.
Pointers
19.3.
Concurrency
20.
Verifying a container library: Binary Search Tree
20.1.
First draft
20.2.
Encapsulating well-formedness with type invariants
20.3.
Making it generic
20.4.
Implementing Clone
20.5.
Full source for the examples
21.
Interacting with unverified code
21.1.
Calling unverified code from verified code
21.2.
Calling verified code from unverified code
22.
Understanding the guarantees of a verified program
22.1.
Assumptions and trusted components
22.2.
Memory safety is conditional on verification
22.3.
Calling verified code from unverified code
Installation, configuration, and tooling
23.
Installation and setup
23.1.
IDE Support
23.2.
Installing and configuring Singular
24.
Project setup and development
24.1.
Working with crates
24.2.
Invoking Verus code from Rust
24.3.
Documentation with Rustdoc
Reference
25.
Supported and unsupported Rust features
26.
Verus syntax by example
27.
Modes
27.1.
Function modes
27.2.
Variable modes
28.
Spec expressions
28.1.
Rust subset
28.2.
Operator Precedence
28.3.
Arithmetic
28.4.
Bit operators
28.5.
Coercion with as
28.6.
Spec equality (==)
28.7.
Extensional equality (=~=, =~~=)
28.8.
Prefix and/or (&&& and |||)
28.9.
Chained operators
28.10.
Implication (==>, <==, and <==>)
28.11.
Quantifiers (forall, exists)
28.12.
Such that (choose)
28.13.
Trigger annotations
28.14.
The view function @
28.15.
Spec index operator []
28.16.
decreases_to!
29.
Proof features
29.1.
assert and assume
29.2.
assert ... by
29.3.
assert forall ... by
29.4.
assert ... by(bit_vector)
29.5.
assert ... by(nonlinear_arith)
29.6.
assert ... by(compute) / by(compute_only)
29.7.
reveal, reveal_with_fuel, hide
30.
Function specifications
30.1.
Function Signatures
30.1.1.
Exec fn signature
30.1.2.
Proof fn signature
30.1.3.
Spec fn signature
30.2.
Signature clauses
30.2.1.
requires / ensures
30.2.2.
returns
30.2.3.
opens_invariants
30.2.4.
no_unwind
30.2.5.
recommends
30.3.
Traits and signature inheritance
30.4.
Specifications on FnOnce
31.
Loop specifications
31.1.
invariant
31.2.
invariant_except_break / ensures
32.
Recursion and termination
32.1.
decreases ... when ... via ...
32.2.
Datatype ordering
32.3.
Cyclic definitions
33.
Type invariants
34.
Attribute list
35.
Directives
35.1.
assume_specification
35.2.
global
36.
Misc. Rust features
36.1.
Statics
36.2.
char
36.3.
Unions
36.4.
Pointers and cells
37.
Command line
37.1.
--record
38.
Planned future work
Light (default)
Rust
Coal
Navy
Ayu
Verus Tutorial and Reference
recommends
See
this guide page
for motivation and overview.