Skip to content

hax

Tutorial

Initializing search

hax
Manual
Frontend
Blog
Publications
Dev

hax

hax
Manual
Manual
- Lean
  Lean
  - Quick start
  - Tutorial
    
    Tutorial
    
    Panic freedom
    
    Proving properties
- F*
  F*
  - Quick start
  - Tutorial
    
    Tutorial
    
    Panic freedom
    
    Proving properties
    
    Data invariants
- Tool versions and proof scenarios
- Faq
  Faq
  - Rust Item Extraction Using cargo hax
Frontend
Frontend
- Evaluation of the hax Frontend
Blog
Blog
- Archive
  Archive
  - 2026
  - 2025
Publications
Dev
Dev
- Architecture
- Grammar of the supported Rust subset

hax
Manual
Lean
Tutorial

Tutorial

This tutorial focuses on proving properties with the hax toolchain and its Lean backend.

Made with Material for MkDocs