1.
Introduction
2.
Quick start
3.
Tutorial
3.1.
Panic freedom
3.2.
Properties on functions
3.3.
Data invariants
4.
Examples
4.1.
Rust By Example
4.2.
Using the F* backend
4.3.
Using the Coq backend
4.4.
Using the ProVerif backend
5.
Proofs
5.1.
F*
5.2.
Coq
5.3.
libcore
6.
Troubleshooting/FAQ
6.1.
Command line usage
6.1.1.
The include flag: which items should be extracted, and how?
7.
Contributing
7.1.
Structure
7.2.
Hax Cargo subcommand
7.3.
Frontend: the Rustc driver
7.4.
Frontend: the exporter
7.5.
Engine
7.6.
Backends
7.7.
Utilities
7.8.
Libraries & Macros
7.9.
libcore
Contributors
Archive
Light
Rust
Coal
Navy
Ayu
hax
Using the ProVerif backend