Verifying Rust cryptography in SymCrypt, from standards to code

Verifying Rust cryptography in SymCrypt, from standards to code - Microsoft Research

Skip to main content

Research

Publications Code & data People Microsoft Research blog

Artificial intelligence Audio & acoustics Computer vision Graphics & multimedia Human-computer interaction Human language technologies Search & information retrieval

Data platforms and analytics Hardware & devices Programming languages & software engineering Quantum computing Security, privacy & cryptography Systems & networking

Algorithms Mathematics

Ecology & environment Economics Medical, health & genomics Social sciences Technology for emerging markets

Academic programs Events & academic conferences Microsoft Research Forum

Behind the Tech podcast Microsoft Research blog Microsoft Research Forum Microsoft Research podcast

About Microsoft Research Careers & internships People Emeritus program News & awards Microsoft Research newsletter

Africa AI for Science AI Frontiers Asia-Pacific Cambridge Health Futures India Montreal New England New York City Redmond

Applied Sciences Mixed Reality & AI - Cambridge Mixed Reality & AI - Zurich

Register: Research Forum

Microsoft Security Azure Dynamics 365 Microsoft 365 Microsoft Teams Windows 365

Microsoft AI Azure Space Mixed reality Microsoft HoloLens Microsoft Viva Quantum computing Sustainability

Education Automotive Financial services Government Healthcare Manufacturing Retail

Find a partner Become a partner Partner Network Microsoft Marketplace Software companies

Blog Microsoft Advertising Developer Center Documentation Events Licensing Microsoft Learn Microsoft Research

View Sitemap

Return to Blog Home Microsoft Research Blog

How Rust, Lean, Aeneas, and AI agents are helping scale formal verification for production cryptographic algorithms

At a glance

SymCrypt develops new verified cryptography using Rust, Aeneas, and Lean to provide higher security assurance.

We prove that their code safely and correctly implements standard algorithms, notably for post-quantum cryptography.

We are releasing verified code, specs, properties, and proofs initially for SHA-3 and ML-KEM.

Aeneas allows verifying a large subset of Rust code and provides efficient automation in Lean to support the proof effort.

Agents allow scaling automation by writing proofs that are independently-verifiable.

Introduction and motivation for formal verification

Cryptographic code sits at the foundation of modern computing. It protects operating systems, cloud services, firmware, messaging systems, and the protocols that connect them. Small mistakes can have outsized consequences: a single arithmetic slip, missing bounds check, or incorrect state transition can undermine the security of an otherwise sound design.

Testing and auditing remain essential, but they are not enough on their own. Cryptographic implementations are often optimized, constant-time, architecture-specific, and deliberately low level. The code that ships rarely looks like the clean algorithm in a standard: it contains reductions, bit manipulations, SIMD intrinsics, carefully shaped loops, and portability layers for many environments.

Formal verification addresses this gap by deploying machine-checked proofs instead of relying on testing alone. Rather than merely checking that the code usually behaves correctly, verification implements a precise mathematical specification for all inputs that satisfy the stated preconditions.

In June last year, Microsoft announced we would formally verify new algorithms written in Rust in SymCrypt , the cryptographic provider used across products and services including Windows and Azure. New cryptographic implementations are being written in safe Rust, then verified in the Lean (opens in new tab) formal proof framework using the Aeneas (opens in new tab) toolchain. This applies in particular to post-quantum cryptography, which require fast secure implementations of complex algorithms. This combination gives us two layers of assurance: Rust rules out broad classes of memory-safety bugs, while Lean proofs establish functional correctness against formal specifications derived from standards.

The result is a new verification methodology for production cryptography: verify code as developers write it, preserve performance-oriented implementation choices, and make the proof process scalable enough to keep up with an evolving codebase.

Figure 1. Agents (stochastic, in blue) and tools (algorithmic, in green) for software verification. Human effort focuses on reviewing formalization of standards and main properties. Agents write proofs and intermediate properties. Compilation, code extraction, and proof verification are deterministic, not agentic.

Status of verification in SymCrypt

We have open sourced a SymCrypt branch (opens in new tab) that includes formal specifications and proofs. This public branch makes the proof artifacts available alongside the Rust algorithm implementations they validate, showing how the methodology applies to production cryptographic code. SymCrypt is not a standalone research prototype; it is Microsoft’s open-source cryptographic library used across products and services including Windows and Azure Linux.

This first release includes complete proofs for the Rust ML-KEM and SHA3 code that is being used in insiders builds of Windows today. SymCrypt is extending the same Rust, Lean, and Aeneas-based workflow to more Rust-native algorithms and integrating them into production versions for Windows and Linux, including for instance verified Rust code for, e.g., AES-GCM, FrodoKEM, and ML-DSA. The rest of this post uses this SymCrypt work as a concrete example, starting with how public standards become executable Lean specifications.

Turning standards into formal Lean specifications

The first step is to formalize what the algorithm is supposed to do. For cryptographic primitives, the source of truth is usually a public standard: a NIST specification, an IETF RFC, or another carefully reviewed algorithm description.

In our approach, the Lean specification is designed to stay close to the standard. When the standard describes a loop, an array update, or a mathematical operation, the Lean model follows the same structure wherever possible. This syntactic proximity matters: it makes the formal specification easier to audit because reviewers can compare the standard and the Lean side by side.

Lean also lets us write executable specifications. That means we...