Verus overview
Getting started
Getting started
Tutorial
Basic specifications
Specification code, proof code, executable code
Recursion and loops
Datatypes: struct and enum
1. Defining datatypes
2. Querying the discriminant (#[is_variant])
3. Proving properties of fields
Basic libraries and spec closures
Quantifiers
Higher-order executable functions
1. Passing functions as values
2. Closures
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
Improving SMT performance
1. Modules, hiding, opaque, reveal
2. Quantifier profiling
3. Hiding local proofs with assert (...) by { ... }
4. Structured proof by calculation
5. Proof by computation
6. Spinning off separate SMT queries
7. Breaking proofs into smaller pieces
Mutation, references, and borrowing
1. Requires and ensures with mutable references
2. Assertions containing mutable references
Traits
Ghost and tracked variables
Concurrency and Unsafe Code
Attributes and directives
1. external and external_body
2. inline
3. opaque
4. decreases_by
5. when_used_as_spec
Strings
1. String library
2. String literals
Macros
Tools and command-line options
1. Proof Debugger
2. IDE Support
3. Syntax Highlighting
Verification and Rust
1. Why Rust?
2. Supported Rust features
3. Borrowing and lifetimes
4. Mutable borrows
5. Interior mutability
6. Alternatives to unsafe
Understanding the guarantees of a verified program
1. Assumptions and trusted components
2. Identifying a project's TCB
3. Memory safety is conditional on verification
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 overview
Modes
1. Function modes
2. Variable modes
Spec expressions
1. Rust subset
2. Arithmetic
3. Spec equality (==)
4. Extensional equality (=~=, =~~=)
5. Prefix and/or (&&& and |||)
6. Chained operators
7. Implication (==>, <==, and <==>)
8. Quantifiers (forall, exists)
9. Such that (choose)
10. Function expressions
11. Trigger annotations
12. The view function @
13. Spec index operator []
Proof features
1. assert and assume
2. assert ... by
3. assert forall ... by
4. assert ... by(bit_vector)
5. assert ... by(nonlinear_arith)
6. assert ... by(compute) / by(compute_only)
7. reveal
8. fuel
Function specifications
1. requires / ensures
2. opens_invariants
3. recommends
Loop specifications
1. invariant
2. invariant_except_break / ensures
Recursion and termination
1. decreases ...
2. decreases ... when ...
3. decreases ... via ...
4. Datatype ordering
5. Cyclic definitions
Misc. Rust features
1. Statics
2. char
Command line
1. --record
Planned future work

Chained operators

In spec code, equality and inequality operators can be chained. For example, a <= b < c is equivalent to a <= b && b < c.

Chained inequalities support <, <=, >, >=, and ==, and support sequences of chained operators of arbitrary length.

Verus Tutorial and Reference

Chained operators