Verus overview
Getting started
Getting started
Tutorial: Fundamentals
Basic specifications
Specification code, proof code, executable code
Recursion and loops
Datatypes: struct and enum
1. Struct
2. Enum
Libraries
1. Specification libraries: Seq, Set, Map
2. Executable libraries: Vec
Spec closures
Tutorial: Understanding the prover
Using assert and assume to develop proofs
Quantifiers
SMT solving, automation, and where automation fails
1. What's decidable, what's undecidable, what's fast, what's slow
2. Integers and nonlinear arithmetic
3. Bit vectors and bitwise operations
4. forall and exists: writing and using triggers, inline functions
5. Recursive functions
6. Extensional equality
7. Libraries: incomplete axioms for Seq, Set, Map
Managing proof performance and why it's critical
1. Measuring verification performance
2. Quantifier profiling
3. Modules, hiding, opaque, reveal
4. Hiding local proofs with assert (...) by { ... }
5. Structured proof by calculation
6. Proof by computation
7. Spinning off separate SMT queries
8. Breaking proofs into smaller pieces
Checklist: what to do when proofs go wrong
Tutorial: Verification and Rust
Mutation, references, and borrowing
1. Requires and ensures with mutable references
2. Assertions containing mutable references
Traits
Higher-order executable functions
1. Passing functions as values
2. Closures
Ghost and tracked variables
Strings
1. String library
2. String literals
Macros
Unsafe code & complex ownership
Verifying a container library: Binary Search Tree
Understanding the guarantees of a verified program
Installation, configuration, and tooling
Installation and setup
1. IDE Support
2. Installing and configuring Singular
Project setup and development
1. Working with crates
2. Invoking Verus code from Rust
3. Documentation with Rustdoc
Reference
Supported and unsupported Rust features
Verus syntax by example
Modes
1. Function modes
2. Variable modes
Spec expressions
Proof features
Function specifications
1. requires / ensures
2. opens_invariants
3. no_unwind
4. Traits and signature inheritance
5. Specifications on FnOnce
6. recommends
Loop specifications
1. invariant
2. invariant_except_break / ensures
Recursion and termination
1. decreases ... when ... via ...
2. Datatype ordering
3. Cyclic definitions
Type invariants
Attribute list
The "global" directive
Misc. Rust features
Command line
1. --record
Planned future work

Verus Tutorial and Reference

Spec expressions

Many built-in operators are in spec mode, i.e., they can be used in specification expressions. This section discusses those operators.