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, ISet, Map, IMap
    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
    1. 17.1. Finite Iterators
    2. 17.2. Infinite Iterators
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. Logical atomicity
    1. 23.1. Atomic specifications
    2. 23.2. Invoking the linearization point
    3. 23.3. Calling a logically atomic function
33. 24. Verifying a container library: Binary Search Tree
    1. 24.1. First draft
    2. 24.2. Encapsulating well-formedness with type invariants
    3. 24.3. Making it generic
    4. 24.4. Implementing Clone
    5. 24.5. Mutable references in a container
    6. 24.6. Full source for the examples
34. 25. Interacting with unverified code
    1. 25.1. Calling unverified code from verified code
    2. 25.2. Calling verified code from unverified code
35. 26. Understanding the guarantees of a verified program
    1. 26.1. Assumptions and trusted components
    2. 26.2. Memory safety is conditional on verification
    3. 26.3. Calling verified code from unverified code
37. Installation, configuration, and tooling
38. 27. Installation and setup
    1. 27.1. IDE Support
    2. 27.2. Installing and configuring Singular
39. 28. Project setup and development
    1. 28.1. Using Verus via Cargo
    2. 28.2. Documentation with Rustdoc
    3. 28.3. Ghost Erasure
41. Reference
42. 29. Supported and unsupported Rust features
43. 30. Verus syntax by example
44. 31. Modes
    1. 31.1. Function modes
    2. 31.2. Variable modes
45. 32. Contributed Extensions
    1. 32.1. Automatic spec to exec functions
    2. 32.2. Spec and proof attributes for exec functions
       1. 32.2.1. Automatic exec to spec functions
46. 33. Specification language
    1. 33.1. Type Interpretations
    2. 33.2. Spec expressions
       1. 33.2.1. Operator Precedence
       2. 33.2.2. Rust subset
       3. 33.2.3. Arithmetic
       4. 33.2.4. Bit operators
       5. 33.2.5. Coercion with as
       6. 33.2.6. Spec equality (==)
       7. 33.2.7. Extensional equality (=~=, =~~=)
       8. 33.2.8. Prefix and/or (&&& and |||)
       9. 33.2.9. Chained operators
       10. 33.2.10. Implication (==>, <==, and <==>)
       11. 33.2.11. Quantifiers (forall, exists)
       12. 33.2.12. Such that (choose)
       13. 33.2.13. Trigger annotations
       14. 33.2.14. The view function @
       15. 33.2.15. Spec index operator []
       16. 33.2.16. The has operator
       17. 33.2.17. The is operator
       18. 33.2.18. The matches operator
       19. 33.2.19. decreases_to!
47. 34. Proofs
    1. 34.1. Proof statements
       1. 34.1.1. assert
       2. 34.1.2. assume
       3. 34.1.3. assert ... by
       4. 34.1.4. assert forall ... by
       5. 34.1.5. assert ... by(...)
       6. 34.1.6. reveal, reveal_with_fuel, hide
       7. 34.1.7. reveal_strlit
    2. 34.2. Prover modes
       1. 34.2.1. "default" mode
       2. 34.2.2. bit_vector
       3. 34.2.3. nonlinear
       4. 34.2.4. integer_ring
       5. 34.2.5. compute/compute_only
48. 35. Function specifications
    1. 35.1. Function Signatures
       1. 35.1.1. Exec fn signature
       2. 35.1.2. Proof fn signature
       3. 35.1.3. Spec fn signature
    2. 35.2. Signature clauses
       1. 35.2.1. requires / ensures
       2. 35.2.2. returns
       3. 35.2.3. opens_invariants
       4. 35.2.4. no_unwind
       5. 35.2.5. recommends
    3. 35.3. Traits and signature inheritance
    4. 35.4. Specifications on FnOnce
49. 36. External trait specifications
50. 37. Loop specifications
    1. 37.1. invariant
    2. 37.2. invariant_except_break / ensures
51. 38. Recursion and termination
    1. 38.1. decreases ... when ... via ...
    2. 38.2. Datatype ordering
    3. 38.3. Cyclic definitions
52. 39. Type invariants
53. 40. Attribute list
54. 41. Directives
    1. 41.1. assume_specification
    2. 41.2. global
55. 42. Misc. Rust features
    1. 42.1. Statics
    2. 42.2. Unions
    3. 42.3. Pointers and cells
56. 43. Command line
    1. 43.1. --record
57. 44. Planned future work