Verus overview
Getting started
Getting started
1. ... on the command line
2. ... with VSCode
Tutorial: Fundamentals
Using Verus within Rust
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
Developing 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 proofs 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 about mutable references
Traits
Higher-order executable functions
1. Passing functions as values
2. Closures
Ghost and tracked variables
Strings
Macros
Unsafe code & complex ownership
Verifying a container library: Binary Search Tree
Interacting with unverified code
1. Calling unverified code from verified code
2. Calling verified code from unverified code
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
Contributed Extensions
Spec expressions
Proof features
Function specifications
1. Function Signatures
3. Signature clauses
4. 1. requires / ensures
  2. returns
  3. opens_invariants
  4. no_unwind
  5. recommends
5. Traits and signature inheritance
6. Specifications on FnOnce
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
Directives
1. assume_specification
2. global
Misc. Rust features
Command line
1. --record
Planned future work

Verus Tutorial and Reference

Extensional equality (`=~=` and `=~~=`)

The extensional equality operators =~= and =~~= are explained in Extensional equality.