hax

Hax translates Rust code into formal languages such as Lean, F*, and ProVerif, so you can prove that your code is panic-free, functionally correct, and meets its security goals.

Read the docs Try the playground GitHub

How it works

  1. Write Rust, state what it should do

    Contracts are ordinary Rust attributes from hax_lib.

    #[hax_lib::requires(x < 16)]
#[hax_lib::ensures(|res| res >= x)]
pub fn square(x: u8) -> u8 {
    x * x
}

  2. Extract to a proof assistant

    One command translates the crate into Lean, F*, or ProVerif.

    cargo hax into lean

  3. Prove it

    The contract becomes a theorem about the extracted code.

    @[spec]
theorem square.spec.proof (x : Std.U8) : square.spec x := by
  unfold square.spec square
  hax_mvcgen
  all_goals grind [Nat.le_mul_self]

Try it outFull tutorial

More reading

News

Community

Questions and discussion on Zulip, issues and contributions on GitHub.

Funding