Skip to content

hax

Tutorial

Initializing search

hax
Manual
Engine
Frontend
Blog
Publications
Dev

hax

hax
Manual
Manual
- F*
  F*
  - Quick start
  - Tutorial
    
    Tutorial
    
    Panic freedom
    
    Proving properties
    
    Data invariants
- Lean
  Lean
  - Quick start
  - Tutorial
    
    Tutorial
    
    Panic freedom
    
    Proving properties
  - Internals
- Faq
  Faq
  - Rust Item Extraction Using cargo hax
  - Troubleshooting/FAQ
Engine
Engine
- Toolchain structure
  Toolchain structure
Frontend
Frontend
- Evaluation of the hax Frontend
Blog
Blog
- Archive
  Archive
  - 2025
Publications
Dev
Dev
- Architecture
- Ast ebnf
- Docs
- Libraries

Tutorial

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

Made with Material for MkDocs