Microsoft has released machine-checked proofs for Rust implementations of SHA-3 and ML-KEM in SymCrypt, its production cryptographic library used across Windows and Azure Linux. Announced by Microsoft Research on July 13, the work combines Rust, the Lean proof assistant, the Aeneas verification toolchain, and AI agents to establish that selected implementations correctly follow their formal specifications.
The verified ML-KEM and SHA-3 code is already being used in Windows Insider builds, according to Microsoft, although the company did not identify specific builds or channels. The public SymCrypt branch includes the Rust code alongside its specifications, properties, and proofs, giving security researchers a chance to inspect more than a polished research demonstration.
This is an important distinction. Microsoft is not merely verifying a simplified reference implementation and then separately maintaining faster production code. Its stated goal is to prove properties about the optimized, multi-architecture Rust implementations that Windows and other products can actually ship.
Microsoft announced its broader plan to rewrite parts of SymCrypt in Rust in June 2025. SymCrypt remains a foundational library rather than a user-facing Windows feature: applications and operating-system components call its cryptographic functions to perform hashing, encryption, signing, verification, and key establishment.
Moving new algorithms from C to safe Rust helps eliminate broad categories of memory-safety errors, including invalid memory access and many lifetime or aliasing mistakes. That is valuable for cryptographic code, but memory safety alone cannot prove that an algorithm performs the right mathematical operation.
A perfectly memory-safe implementation could still calculate the wrong value, mishandle an edge case, or depart subtly from a standard. Microsoft is therefore using Lean to prove functional correctness: for inputs meeting the theorem’s stated preconditions, the implementation produces the result defined by a formal specification derived from the relevant standard.
The two layers address different risks. Rust constrains how the program uses memory, while Lean checks whether the modeled implementation agrees with the declared mathematical behavior. Neither layer should be mistaken for a universal proof that the entire cryptographic system is invulnerable.
Formal verification is only as meaningful as the property being proved, the specification against which it is checked, and the assumptions surrounding low-level components. Microsoft’s publication of those artifacts matters because external reviewers can examine whether the theorem actually captures the security-relevant behavior developers expect.
The specification is also executable. Engineers can run it against official test vectors, helping catch transcription mistakes, off-by-one errors, and misunderstandings before treating the model as the reference against which production code will be proved.
Microsoft Research uses the number-theoretic transform in ML-KEM as a representative example. ML-KEM is the standardized post-quantum key-encapsulation mechanism descended from CRYSTALS-Kyber, and its implementation involves structured polynomial arithmetic that must be both fast and exact.
The Lean model mirrors the standard’s loops, coefficient updates, and mathematical operations. Microsoft can then prove higher-level properties about that model, such as whether the transformation corresponds to the intended operation over the relevant polynomial ring.
Aeneas provides the bridge from implementation to proof. It translates Rust’s mid-level representation into a pure model that Lean can reason about. A Rust routine that mutates an array in place can become a functional Lean representation that accepts an array and returns its updated value, including a result indicating whether execution can panic.
The central theorem can then state that the translated Rust function refines the standard-derived specification. Put more plainly, the proof checks that the real implementation and the formal description produce the same mathematical result under the documented conditions.
This separation is central to Microsoft’s engineering pitch. Cryptographic developers can continue writing idiomatic, performance-oriented Rust, rather than reshaping every routine around a specialized verification language. Proof engineers work with the generated Lean model and theorems without inserting proof annotations throughout the shipping Rust implementation.
SymCrypt must operate in environments ranging from Windows kernel components and firmware to cloud services. A proof covering only a portable fallback would therefore leave some of the most performance-critical paths outside the guarantee.
Microsoft says its toolchain compiles the Rust code separately for each target that needs verification and then merges those models. For the ML-KEM implementation discussed in the research post, this includes x86-64 and Arm64 paths, with dispatch to XMM, Neon, or generic routines where appropriate.
Hardware intrinsics require additional assumptions. Low-level wrappers involving raw pointers or processor instructions may be represented by small Lean specifications that must be carefully reviewed. Other intrinsics can be modeled in Rust, checked against hardware documentation, and subsequently translated.
That approach narrows the portion of the system that must be trusted without pretending it disappears. It also highlights one of the release’s most consequential claims: formal verification does not necessarily require abandoning SIMD acceleration or architecture-specific optimization.
For Windows administrators, there is no new policy to deploy and no switch to enable. The immediate effect is upstream: future Windows cryptographic operations can inherit stronger assurance as verified SymCrypt implementations move from Insider testing into production releases.
Microsoft has not supplied a general-availability schedule for the verified SHA-3 or ML-KEM paths. It also has not said that every SymCrypt algorithm, platform-specific routine, or caller is now formally verified.
Microsoft argues that agents can perform repetitive work such as unfolding generated models, applying helper-function specifications, resolving arithmetic obligations, and repairing proofs after refactoring. Human specialists can spend more time defining the important properties, reviewing assumptions, and checking whether theorem statements provide the intended guarantee.
The reliability boundary is different from ordinary AI-generated code. An agent can propose a Lean proof, but Lean’s trusted kernel independently checks whether that proof is valid. A plausible-looking but logically invalid script is rejected rather than accepted on the strength of the model’s confidence.
That does not eliminate the human-review problem. An agent might help formalize the wrong interpretation of a standard, and a valid proof of a weak theorem may provide little useful assurance. Trusted models for intrinsics and hardware behavior also remain part of the security boundary.
Microsoft is addressing visibility with automatically generated dashboards that expose covered functions, preconditions, postconditions, trusted models, and outstanding assumptions. When the Rust code changes, its Lean models and proofs can be regenerated; a broken proof then becomes an engineering signal rather than a research artifact discovered months later.
The real scaling test is whether this survives continuous product development. Proofs must remain synchronized with compiler targets, optimized implementations, revised standards, and the steady refactoring expected in a library used across Windows and Azure.
Microsoft says it is extending the workflow to additional Rust-native SymCrypt algorithms, including AES-GCM, FrodoKEM, and ML-DSA. That wording describes ongoing work, not a declaration that all those implementations are already verified or shipping broadly.
Functional proofs also do not replace testing, audits, cryptanalysis, or side-channel analysis. Microsoft’s earlier SymCrypt roadmap separately discussed examining compiled binaries for timing and microarchitectural leakage, acknowledging that source-level correctness does not prove that secrets cannot escape through processor behavior.
The July 13 release is therefore best read as a concrete checkpoint rather than the end of the project. Microsoft now has public proof artifacts for two production-relevant algorithms and verified code running in Windows Insider builds; the next milestone is moving those guarantees into stable Windows releases without losing performance, platform coverage, or maintainability.
The verified ML-KEM and SHA-3 code is already being used in Windows Insider builds, according to Microsoft, although the company did not identify specific builds or channels. The public SymCrypt branch includes the Rust code alongside its specifications, properties, and proofs, giving security researchers a chance to inspect more than a polished research demonstration.
This is an important distinction. Microsoft is not merely verifying a simplified reference implementation and then separately maintaining faster production code. Its stated goal is to prove properties about the optimized, multi-architecture Rust implementations that Windows and other products can actually ship.
Rust Removes One Bug Class, Lean Tackles Another
Microsoft announced its broader plan to rewrite parts of SymCrypt in Rust in June 2025. SymCrypt remains a foundational library rather than a user-facing Windows feature: applications and operating-system components call its cryptographic functions to perform hashing, encryption, signing, verification, and key establishment.Moving new algorithms from C to safe Rust helps eliminate broad categories of memory-safety errors, including invalid memory access and many lifetime or aliasing mistakes. That is valuable for cryptographic code, but memory safety alone cannot prove that an algorithm performs the right mathematical operation.
A perfectly memory-safe implementation could still calculate the wrong value, mishandle an edge case, or depart subtly from a standard. Microsoft is therefore using Lean to prove functional correctness: for inputs meeting the theorem’s stated preconditions, the implementation produces the result defined by a formal specification derived from the relevant standard.
The two layers address different risks. Rust constrains how the program uses memory, while Lean checks whether the modeled implementation agrees with the declared mathematical behavior. Neither layer should be mistaken for a universal proof that the entire cryptographic system is invulnerable.
Formal verification is only as meaningful as the property being proved, the specification against which it is checked, and the assumptions surrounding low-level components. Microsoft’s publication of those artifacts matters because external reviewers can examine whether the theorem actually captures the security-relevant behavior developers expect.
Standards Become Executable Specifications
The workflow begins by translating public cryptographic standards into Lean specifications. Microsoft says these models are intentionally kept close to the source documents, allowing reviewers to compare the standard and formal version with less interpretive distance.The specification is also executable. Engineers can run it against official test vectors, helping catch transcription mistakes, off-by-one errors, and misunderstandings before treating the model as the reference against which production code will be proved.
Microsoft Research uses the number-theoretic transform in ML-KEM as a representative example. ML-KEM is the standardized post-quantum key-encapsulation mechanism descended from CRYSTALS-Kyber, and its implementation involves structured polynomial arithmetic that must be both fast and exact.
The Lean model mirrors the standard’s loops, coefficient updates, and mathematical operations. Microsoft can then prove higher-level properties about that model, such as whether the transformation corresponds to the intended operation over the relevant polynomial ring.
Aeneas provides the bridge from implementation to proof. It translates Rust’s mid-level representation into a pure model that Lean can reason about. A Rust routine that mutates an array in place can become a functional Lean representation that accepts an array and returns its updated value, including a result indicating whether execution can panic.
The central theorem can then state that the translated Rust function refines the standard-derived specification. Put more plainly, the proof checks that the real implementation and the formal description produce the same mathematical result under the documented conditions.
This separation is central to Microsoft’s engineering pitch. Cryptographic developers can continue writing idiomatic, performance-oriented Rust, rather than reshaping every routine around a specialized verification language. Proof engineers work with the generated Lean model and theorems without inserting proof annotations throughout the shipping Rust implementation.
Verification Follows the Optimized Code Paths
Production cryptography rarely resembles a clean textbook algorithm. It contains fixed-width arithmetic, carefully controlled loops, CPU feature detection, vector instructions, portability layers, and different paths for different architectures.SymCrypt must operate in environments ranging from Windows kernel components and firmware to cloud services. A proof covering only a portable fallback would therefore leave some of the most performance-critical paths outside the guarantee.
Microsoft says its toolchain compiles the Rust code separately for each target that needs verification and then merges those models. For the ML-KEM implementation discussed in the research post, this includes x86-64 and Arm64 paths, with dispatch to XMM, Neon, or generic routines where appropriate.
Hardware intrinsics require additional assumptions. Low-level wrappers involving raw pointers or processor instructions may be represented by small Lean specifications that must be carefully reviewed. Other intrinsics can be modeled in Rust, checked against hardware documentation, and subsequently translated.
That approach narrows the portion of the system that must be trusted without pretending it disappears. It also highlights one of the release’s most consequential claims: formal verification does not necessarily require abandoning SIMD acceleration or architecture-specific optimization.
For Windows administrators, there is no new policy to deploy and no switch to enable. The immediate effect is upstream: future Windows cryptographic operations can inherit stronger assurance as verified SymCrypt implementations move from Insider testing into production releases.
Microsoft has not supplied a general-availability schedule for the verified SHA-3 or ML-KEM paths. It also has not said that every SymCrypt algorithm, platform-specific routine, or caller is now formally verified.
AI Writes Proofs, but Lean Gets the Final Vote
The more novel part of Microsoft’s process is its use of AI agents to draft specifications and produce or repair proof scripts. Formal verification has historically required large amounts of specialist labor, making it difficult to apply continuously across a fast-changing production codebase.Microsoft argues that agents can perform repetitive work such as unfolding generated models, applying helper-function specifications, resolving arithmetic obligations, and repairing proofs after refactoring. Human specialists can spend more time defining the important properties, reviewing assumptions, and checking whether theorem statements provide the intended guarantee.
The reliability boundary is different from ordinary AI-generated code. An agent can propose a Lean proof, but Lean’s trusted kernel independently checks whether that proof is valid. A plausible-looking but logically invalid script is rejected rather than accepted on the strength of the model’s confidence.
That does not eliminate the human-review problem. An agent might help formalize the wrong interpretation of a standard, and a valid proof of a weak theorem may provide little useful assurance. Trusted models for intrinsics and hardware behavior also remain part of the security boundary.
Microsoft is addressing visibility with automatically generated dashboards that expose covered functions, preconditions, postconditions, trusted models, and outstanding assumptions. When the Rust code changes, its Lean models and proofs can be regenerated; a broken proof then becomes an engineering signal rather than a research artifact discovered months later.
The real scaling test is whether this survives continuous product development. Proofs must remain synchronized with compiler targets, optimized implementations, revised standards, and the steady refactoring expected in a library used across Windows and Azure.
Post-Quantum Code Is the First Production Test
Starting with ML-KEM gives the project practical urgency. Post-quantum migration requires organizations to adopt comparatively new implementations of mathematically complex algorithms across operating systems, protocols, services, and hardware platforms.Microsoft says it is extending the workflow to additional Rust-native SymCrypt algorithms, including AES-GCM, FrodoKEM, and ML-DSA. That wording describes ongoing work, not a declaration that all those implementations are already verified or shipping broadly.
Functional proofs also do not replace testing, audits, cryptanalysis, or side-channel analysis. Microsoft’s earlier SymCrypt roadmap separately discussed examining compiled binaries for timing and microarchitectural leakage, acknowledging that source-level correctness does not prove that secrets cannot escape through processor behavior.
The July 13 release is therefore best read as a concrete checkpoint rather than the end of the project. Microsoft now has public proof artifacts for two production-relevant algorithms and verified code running in Windows Insider builds; the next milestone is moving those guarantees into stable Windows releases without losing performance, platform coverage, or maintainability.
References
- Primary source: Microsoft
Published: 2026-07-13T16:00:00+00:00
Verifying Rust cryptography in SymCrypt, from standards to code - Microsoft Research
Cryptographic code supports vital protections in modern computing systems. Learn how a new method helps verify code as developers write it while preserving speed and adaptability as it gets implemented and evolves:www.microsoft.com
