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