1. Introduction
2. 1. Brief introduction to VeriFast for Rust
3. 2. Symbolic execution states
4. 3. Annotations
5. 1. 3.1. Keywords
   2. 3.2. Types
   3. 3.3. Expressions
   4. 3.4. Assertions
   5. 3.5. Function specifications
   6. 3.6. Function body annotations
   7. 3.7. Ghost declarations
6. 4. Verifying compliance with Rust's pointer aliasing rules
7. 5. Verifying non-`unsafe` functions
8. 1. 5.1. The lifetime logic