hax

hax translates a large subset of Rust into formal languages such as Lean, F* and Rocq, so that you can prove your code does what it should.

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 Rocq.

    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]

From the Lean tutorial.

News

Community

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