1. Introduction
2. 1. Symbolic execution states
3. 2. Annotations
4. 1. 2.1. Keywords
   2. 2.2. Types
   3. 2.3. Expressions
   4. 2.4. Assertions
   5. 2.5. Function specifications
   6. 2.6. Function body annotations
   7. 2.7. Ghost declarations
5. 3. Verifying compliance with Rust's pointer aliasing rules
6. 4. Verifying non-`unsafe` functions