It’s not an academic nuance: formal verification of cryptographic code is becoming an operational requirement for those running sensitive workloads in controlled environments. Microsoft has just open-sourced a branch of SymCrypt, the library that secures Windows and Azure, with mathematical proofs demonstrating the correctness of its Rust implementations of SHA-3 and ML-KEM. The work, carried out with the Lean proof assistant and the Aeneas translator, marks a shift from trusting tests to relying on machine-checked certainty.

From the NIST standard to a verifiable model

The starting point is the public specification: for ML-KEM’s number-theoretic transform (NTT), for instance, the algorithm is translated nearly line-by-line into Lean, preserving the loop structure and coefficient updates. This syntactic proximity is not a stylistic whim—it allows human reviewers to inspect the formal model side-by-side with the standard. Moreover, the model is executable, so it can be tested against official vectors before any Rust code is touched.

Aeneas then takes the Rust function engineers wrote—with in-place array mutations, optimizations, memory management—and turns it into a pure functional model inside Lean. Rust’s borrow checking eliminates whole classes of reasoning about aliasing and mutability, simplifying the proof. The final theorem states: for every input satisfying the preconditions, the implementation returns the same result as the standard-derived model. Nothing less.

Multi-architecture optimizations under scrutiny

Real-world cryptography cannot ignore hardware. SymCrypt uses SSE2 intrinsics on x86-64 and Neon on aarch64, with dynamic dispatch. To verify these paths as well, the toolchain compiles the Rust code for each target, produces separate Lean models, and then merges them into a single theorem covering all variants. Where low-level wrappers are needed, small, manually reviewed Lean specifications are written: the trusted surface remains minimal, while performance stays intact.

This is the point that should interest those managing on-premise or air-gapped servers. Knowing that the cryptographic algorithms—including the post-quantum ones already shipping in Windows Insider builds—are formally aligned with the NIST standard is not a luxury. When running LLM inference locally, model weights and sensitive data flow over channels protected precisely by those primitives. A flaw there would undermine any sovereignty architecture.

Agents in service of proof

Microsoft uses AI agents in two phases: to draft the translation of standards into Lean specifications (later reviewed) and to write and repair proofs. Because Lean has a minimal verification kernel, any agent-proposed script is still validated deterministically. The result is a dramatic acceleration: work that once took months of specialist effort can now be completed much faster, with engineers shifting from hand-writing every lemma to designing the verification strategy and reviewing the final theorems.

Automatically generated dashboards then expose the guarantees in developer-friendly terms: preconditions, postconditions, covered functions, residual assumptions. This allows the Rust developer to independently check whether the theorem truly captures what their function should guarantee, closing the loop between development and formal proof.

The combination of Rust, Lean, Aeneas, and agentic automation redefines the economics of verification. It’s no longer a separate lab exercise but an integrated process that accompanies code into production. For IT decision-makers evaluating on-premise stacks, the presence of verified cryptography downstream of a standard like NIST is a structural signal: trust is not merely delegated to the vendor; it can be (partially) inspected. In an era when quantum threats are starting to be taken seriously, that’s no small detail.