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
       3. 5.3.3. Iterators
    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
14. 9. Quantifiers
    1. 9.1. forall and triggers
    2. 9.2. Multiple variables, multiple triggers, matching loops
    3. 9.3. exists and choose
    4. 9.4. Proofs about forall and exists
    5. 9.5. Example: binary search
    6. 9.6. Ambient (broadcast) lemmas
16. Tutorial: Proof Development
17. 10. Developing proofs
    1. 10.1. Using assert and assume
    2. 10.2. Devising loop invariants
    3. 10.3. Proving absence of overflow
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. Using LLM assistants
    1. 13.1. Using LLMs to develop proofs
    2. 13.2. Using LLMs to develop specifications
21. 14. Checklist: what to do when proofs go wrong
23. Tutorial: Verification and Rust
24. 15. Mutation, references, and borrowing
    1. 15.1. Mutable references
    2. 15.2. Assertions about mutable references
25. 16. Traits
26. 17. Iterator Specifications
27. 18. Higher-order executable functions
    1. 18.1. Passing functions as values
    2. 18.2. Closures
28. 19. Ghost and tracked variables
29. 20. Strings
30. 21. Macros
31. 22. Unsafe code & complex ownership
    1. 22.1. Cells / interior mutability
    2. 22.2. Pointers
    3. 22.3. Concurrency
32. 23. Verifying a container library: Binary Search Tree
    1. 23.1. First draft
    2. 23.2. Encapsulating well-formedness with type invariants
    3. 23.3. Making it generic
    4. 23.4. Implementing Clone
    5. 23.5. Mutable references in a container
    6. 23.6. Full source for the examples
33. 24. Interacting with unverified code
    1. 24.1. Calling unverified code from verified code
    2. 24.2. Calling verified code from unverified code
34. 25. Understanding the guarantees of a verified program
    1. 25.1. Assumptions and trusted components
    2. 25.2. Memory safety is conditional on verification
    3. 25.3. Calling verified code from unverified code
36. Installation, configuration, and tooling
37. 26. Installation and setup
    1. 26.1. IDE Support
    2. 26.2. Installing and configuring Singular
38. 27. Project setup and development
    1. 27.1. Working with crates
    2. 27.2. Invoking Verus code from Rust
    3. 27.3. Documentation with Rustdoc
    4. 27.4. Ghost Erasure
40. Reference
41. 28. Supported and unsupported Rust features
42. 29. Verus syntax by example
43. 30. Modes
    1. 30.1. Function modes
    2. 30.2. Variable modes
44. 31. Contributed Extensions
    1. 31.1. Automatic spec to exec functions
    2. 31.2. Spec and proof attributes for exec functions
       1. 31.2.1. Automatic exec to spec functions
45. 32. Spec expressions
    1. 32.1. Rust subset
    2. 32.2. Operator Precedence
    3. 32.3. Arithmetic
    4. 32.4. Bit operators
    5. 32.5. Coercion with as
    6. 32.6. Spec equality (==)
    7. 32.7. Extensional equality (=~=, =~~=)
    8. 32.8. Prefix and/or (&&& and |||)
    9. 32.9. Chained operators
    10. 32.10. Implication (==>, <==, and <==>)
    11. 32.11. Quantifiers (forall, exists)
    12. 32.12. Such that (choose)
    13. 32.13. Trigger annotations
    14. 32.14. The view function @
    15. 32.15. Spec index operator []
    16. 32.16. decreases_to!
46. 33. Proof features
    1. 33.1. assert and assume
    2. 33.2. assert ... by
    3. 33.3. assert forall ... by
    4. 33.4. assert ... by(bit_vector)
    5. 33.5. assert ... by(nonlinear_arith)
    6. 33.6. assert ... by(compute) / by(compute_only)
    7. 33.7. reveal, reveal_with_fuel, hide
47. 34. Function specifications
    1. 34.1. Function Signatures
       1. 34.1.1. Exec fn signature
       2. 34.1.2. Proof fn signature
       3. 34.1.3. Spec fn signature
    2. 34.2. Signature clauses
       1. 34.2.1. requires / ensures
       2. 34.2.2. returns
       3. 34.2.3. opens_invariants
       4. 34.2.4. no_unwind
       5. 34.2.5. recommends
    3. 34.3. Traits and signature inheritance
    4. 34.4. Specifications on FnOnce
48. 35. External trait specifications
49. 36. Loop specifications
    1. 36.1. invariant
    2. 36.2. invariant_except_break / ensures
50. 37. Recursion and termination
    1. 37.1. decreases ... when ... via ...
    2. 37.2. Datatype ordering
    3. 37.3. Cyclic definitions
51. 38. Type invariants
52. 39. Attribute list
53. 40. Directives
    1. 40.1. assume_specification
    2. 40.2. global
54. 41. Misc. Rust features
    1. 41.1. Statics
    2. 41.2. char
    3. 41.3. Unions
    4. 41.4. Pointers and cells
55. 42. Command line
    1. 42.1. --record
56. 43. Planned future work