As announced in our recent blog post, hax 0.4 has a new Lean backend that relies on Aeneas. In this post, we describe how we used this new backend to verify the SHA-3 implementation in libcrux-iot, an IoT-friendly cryptographic library developed by CE Labs. Our goal was to find out how close we are to a workflow in which a Rust developer without any knowledge of Lean can verify their own code using hax and AI.

The results of the project are publicly available in this GitHub repository.

Of course, we are not the first to prove the correctness of a SHA-3 implementation. We previously verified libcrux’s SHA-3 using hax and F*. Just this year, Apple verified their assembly and C implementations of SHA-3 using a combination of SAW and Isabelle. Microsoft verified a Rust implementation of SHA-3 also using Aeneas and Lean.

What distinguishes the hax approach is that we try to model as much as possible in Rust: the specification is in Rust, and even our models of the Rust core libraries are written in Rust. This allows a Rust developer with no knowledge of Lean to test and review the specifications, assumptions, and target theorems. They can then use hax to generate the Lean, invoke their favorite AI agent to fill in the proofs, and run Lean to verify that the proofs are complete.

The workflow that we followed for SHA-3 is depicted below. The developer works on the red (Rust) parts; the blue (Lean) parts are generated by hax and AI, and checked by Lean.

An IoT-friendly implementation of SHA-3

The libcrux-iot library is a collection of cryptographic algorithms implemented in Rust and targeted at IoT devices and other embedded systems that have low memory and operate on simple (32-bit or smaller) processors. Specialized implementations help to cope with these constraints.

In SHA-3, for example, a central data structure, the lane, is not implemented as a 64-bit integer, as is usually the case. Instead, libcrux-iot uses two 32-bit integers, with all of the even-numbered bits going into one 32-bit integer and the odd-numbered bits into the other, which allows the procedure to be executed more efficiently on 32-bit processors.

The main permutation of SHA-3 consists of 24 rounds of transformations on an internal state, and each round requires an additional working copy of the internal state. The libcrux-iot implementation instead operates fully in-place to save memory, by reorganizing accesses to the internal state such that its layout conforms to the specification only every 4 rounds.

These optimizations make the implementation look very different from the specification.

Specification in Rust

The NIST FIPS 202 standard specifies the SHA-3 algorithm in pseudocode. To be able to verify our implementation against it, we used AI to transcribe SHA-3 into Rust, staying as close as possible to what’s described in the FIPS 202 standard. We call this Rust specification pedantic_sha3.

For example, here is how the standard describes ρ, one of the internal permutation functions used by SHA-3. It permutes the state array, a 5×5×w array of bits, for some constant w that determines its size.

Here is the corresponding part of our Rust specification:

/// Algorithm 2: `ρ(A)`.
pub fn rho<const W: usize>(a: &StateArray<W>) -> StateArray<W> {
    let w = W as i64;
    let mut out = StateArray::<W>::zero();

    // 1. For all z, A′[0, 0, z] = A[0, 0, z].
    for z in 0..W {
        out.a[0][0][z] = a.a[0][0][z];
    }

    // 2. Let (x, y) = (1, 0).
    let (mut x, mut y) = (1usize, 0usize);

    // 3. For t from 0 to 23:
    for t in 0..24i64 {
        // a. A′[x, y, z] = A[x, y, (z - (t+1)(t+2)/2) mod w].
        let offset = (t + 1) * (t + 2) / 2;
        for z in 0..W {
            out.a[x][y][z] = a.a[x][y][imod(z as i64 - offset, w)];
        }
        // b. (x, y) = (y, (2x + 3y) mod 5).
        let (nx, ny) = (y, (2 * x + 3 * y) % 5);
        x = nx;
        y = ny;
    }
    out
}

By comparing them side by side, the developer can check that the specification reflects the standard. Moreover, the Rust specification is executable, so we can increase our confidence by extensive testing. We test the properties stated in the FIPS 202 standard itself, run NIST’s CAVP vectors, and compare with other implementations on random inputs, including a C reference implementation.

An issue we encountered while writing the Rust specification is that Rust arrays are limited to a theoretical maximum of usize::MAX elements (only actually reachable using zero-sized types), which is reflected in hax’s Lean model of Rust arrays. The limit applies to both the implementation and the Rust specification, but there are several reasons why the Rust specification should allow arbitrary lengths:

• FIPS 202 does not impose any limits on the length of the processed messages.

• The Rust specification appends, following FIPS 202, a suffix and padding to the input message, whereas the implementation packs these things more efficiently. So the implementation can handle slightly longer inputs than the specification.

• We would like to use the same Rust specification to also verify the incremental API of SHA-3, which can in theory accept inputs of arbitrary length.

To resolve this, we implemented a special Rust type BitStr for arbitrary-length bitstrings and a special Rust type Nat to hold the length of such a bitstring. In Rust, these are simply wrappers for Vec<u8> and u128, and when executed they have the same limitations as before. But for verification, we exclude their definitions from extraction to Lean and instead define their Lean models to be Lean’s List Bool and Lean’s Nat. So the resulting Lean semantics are exactly what FIPS 202 describes: arbitrary-length bit strings.

Linking the implementation to the specification

To state the correspondence between our implementation and our specification, we use the Rust annotations hax_lib::requires and hax_lib::ensures. For example, for sha256, one of the top-level API functions of the SHA-3 crate, this annotation looks as follows:

#[hax_lib::ensures(|out| out.declassify()[..]
    == pedantic_sha3::bytes::sha3_256(payload.declassify_ref())[..])]
pub fn sha256(payload: &[U8]) -> [U8; SHA3_256_DIGEST_SIZE]

The function computes a 256-bit hash of a given payload.

The hax_lib::ensures-annotation states that the annotated function sha256 does not panic and computes the same value as our specification pedantic_sha3::bytes::sha3_256. The signatures of these two functions differ slightly: The implementation uses a custom integer type U8 that ensures that we use only constant-time integer operations (on the Rust side; not part of the Lean verification). That is why we need to convert U8 into u8 using .declassify() and .declassify_ref(). We must use the “[..]” to work around the fact that hax’s model of Rust core is currently missing the PartialEq implementation for comparing a Vec with an array.

SHA3-256 with an externally allocated buffer

The top-level API functions all come in an external-memory-allocation variant such as sha256_ema. They require the user to provide a digest slice, into which the function writes its output. We annotate it as follows:

#[hax_lib::requires(digest.len() == SHA3_256_DIGEST_SIZE)]
#[hax_lib::ensures(|_| future(digest).declassify_ref()
        == &pedantic_sha3::bytes::sha3_256(payload.declassify_ref())[..])]
pub fn sha256_ema(digest: &mut [U8], payload: &[U8])

The hax_lib::requires-annotation specifies that the digest slice must have the expected length. Otherwise, our verification makes no claims about what the function might do.

The hax_lib::ensures-annotation states the same property as above, but for future(digest), which represents digest’s value after the function has run.

These annotations are the theorems we prove. They are written in Rust, refer only to Rust code, and are what a developer needs to review to know what has been verified.

Extraction to Lean

Implementation, specification, and annotations all get translated via hax into Lean, where we can finally prove that the equivalences hold. For this translation, hax’s new Lean backend uses Aeneas under the hood. For example, the specification’s sha3_256 is defined in Rust as follows:

pub fn sha3_256(m: &BitStr) -> BitStr {
    keccak_c(
        512,
        &m.concat(&BitStr::from_bits(&HASH_SUFFIX)),
        Nat::new(256),
    )
}

hax (via Aeneas) translates this into the following Lean function:

def sha3.sha3_256 (m : bits.BitStr) : RustM bits.BitStr := do
  let s ← lift (Array.to_slice sha3.HASH_SUFFIX)
  let bs ← bits.BitStr.from_bits s
  let bs1 ← bits.BitStr.concat m bs
  let n ← nat.Nat.new 256#u128
  sponge.keccak_c 512#usize bs1 n

The developer does not need to read this code; we show it only to illustrate what hax produces.

Changing the code to aid verification

In a few cases, we had to change the implementation itself to make the Lean extraction work. Most of these changes (e.g., issues with mutability, name clashes) are no longer needed because we fixed lots of bugs both in Aeneas and in hax before releasing hax 0.4. We still have issues with code containing string formatting (e.g., derive(Debug)) and with some unverified parts of the crate (Digest and Hasher impls); these are excluded from extraction.

Another issue we encountered was that the original code contained a couple of functions with 400+ lines of code. While extraction works and proofs are feasible in principle, iterating on these proofs takes too long. Our solution is to use ordinary Rust refactoring to split these functions into smaller ones:

Using hax’s new CLI features

[workspace.dependencies]
hax-lib = { version = "=0.4.2" }

[workspace.metadata.bin]
cargo-hax = { version = "0.4.2", bins = ["cargo-hax"], locked = true }

[alias]
hax = ["bin", "cargo-hax"]

[scenario.pedantic-sha3]
package = "pedantic-sha3"
backend = "lean"

[scenario.libcrux-iot-sha3]
package = "libcrux-iot-sha3"
backend = "lean"
output-dir = "../proofs"

Verification with AI assistance

In Lean, we then proved that the extracted implementation is equivalent to the extracted specification, as stated by the extracted annotations.

The proof uses an intermediate specification of SHA-3 in pure Lean. It proves both the extracted specification and the extracted implementation equivalent to this Lean specification. Finally, it composes these two equivalences to prove the overall correctness theorem.

The proofs were developed almost entirely by AI, with limited human guidance. The proofs are around 15,700 lines long, excluding comments and blank lines. None of this Lean code needs to be reviewed by the developer. The intermediate specification and the proofs are not trusted: Lean checks them, and what they establish is stated by the Rust annotations.

The initial proof development took around a week. We reworked the proof many times: to account for small changes in the implementation, new hax developments, new Lean versions, and changes to the Rust specification. Using AI, keeping up with these changes was surprisingly simple. Even adapting the proofs to a completely different Rust specification took only a couple of hours. Lean played a crucial role here: the fast turnaround and detailed feedback provided by the proof assistant allow the AI agent to easily fix proofs. From our work on verifying libcrux with F*, we have noticed that F* proofs are much harder to maintain, even with AI.

Sometimes, however, the AI got stuck at seemingly simple obstacles.

When Claude Opus 4.7 got stuck

In one situation, Claude Opus 4.7 got stuck because a simp lemma failed to trigger. The underlying reason was a type mismatch in an expression of the form

lift_lane_bv a0 a1 ^^^ lift_lane_bv b0 b1

where both sides were of type BitVec 64 in the simp lemma and of type BitVec U64.numBits in the goal. While U64.numBits is defined as 64, this definition is irreducible, which is why the simp lemma does not trigger. The ^^^-notation hides the mismatch a little, but for a human Lean expert, it’s trivial to hover over the notation and see the underlying issue. In principle, the AI should have the means to find the issue via the Lean MCP server as well.

When Claude Fable 5 got stuck

Even more recent models can go wrong, as shown by the following example, which we encountered using Claude Fable 5 during our work on the verification of ML-KEM, which builds on top of SHA-3. Currently, hax’s hax_lib::implies predicate does not support lazy evaluation. That is, an expression hax_lib::implies(A,B) can panic, even when A evaluates to false. This is a problem because we cannot write expressions like

#[requires(forall(|k| implies(k < a.len(), a[k] <= bound)))]

Here, the array access a[k] can panic when k is too large, and it is modeled to panic even when the condition k < a.len() evaluates to false. A simple workaround is to write

#[requires(forall(|k| if k < a.len() { a[k] <= bound } else { true }))]

For some reason, Fable 5 failed to come up with that workaround and proposed using the following instead:

#[requires(
    let mut ok = true;
    for k in 0..a.len() {
        ok &= a[k] <= bound;
    }
    ok
)]

This formulation would have been much harder to prove properties about.

Note that the fix here is a change to a Rust annotation, which a Rust developer can spot and make without any Lean knowledge. The Opus 4.7 case, by contrast, needed genuine Lean expertise.

Next steps

This verification of SHA-3 still has many limitations and room for improvement:

• Not all top-level API functions have been verified. In particular, we did not verify the incremental API (either buffered or unbuffered), and we did not verify the Digest/Hasher implementations. Also, secret independence is only ensured through Rust type mechanisms, not through Lean.

• Our proofs do not rely on any non-standard Lean axioms, but we’d like to also run comparator to rule out that the AI proved something other than what we stated. This is currently blocked on a Lean upgrade.

• hax does not currently support multi-crate extractions, so the plumbing between implementation and specification crates in Lean is done by hand.

• The hax model of Rust core is still missing a few items that we need in our SHA-3 specification. We currently model them ourselves.

We also see room to improve the proof approach taken by the AI agents. The Lean code generated by hax is designed to be processed by Lean’s verification condition generator mvcgen, but the AI mostly bypassed it: it opened up the monad that hax uses to model Rust computations and worked directly with tactics like rw, simp, omega, and decide. Using mvcgen throughout would separate proofs of panic freedom from proofs of functional correctness, and might make the intermediate Lean specification unnecessary. We expect that more detailed, hax-specific proof skills for the AI will lead to cleaner and more maintainable proofs in the future.

Conclusion

So can a Rust developer without any Lean knowledge verify their own code using hax and AI? For SHA-3, almost. The libcrux-iot code itself was written by Rust developers with no Lean background, and verifying it required only modest Rust-level changes. The verification, admittedly, was carried out by a Lean expert, but for the most part, the steps that need human judgment happen in Rust: specification, contract annotations, modifications of the source code. Lean expertise is still needed in a few places: to fill in missing models, connect multiple crates, and help the AI with the few proofs where it got stuck. We are now working on improving hax to close these gaps. Stay tuned for hax 0.5!