Skip to content

Toolchain structure

Hax is composed of three main parts:

  • The frontend, which interfaces with rustc to extract Rust intermediary representation ASTs (for MIR or THIR) out of Rust code.
  • The engine, which imports the Rust THIR AST to the internal hax AST, and defines a set of transformation phases on this internal AST.
  • The backends, which make use of a set of phases from the engine, and print it to a target verification framework or language. A backend also usually needs to provide a proof library and some more utilities.