Microsoft Uses AI Agents to Verify Rust Cryptography Code
Microsoft Research · rss · 2026-07-14
Microsoft Research published an article detailing how to scale formal verification of production-grade cryptographic algorithms using Rust, Lean, Aeneas, and AI agents.
- Background: Cryptographic code demands extremely high security, which traditional testing cannot fully guarantee. Microsoft rewrote algorithms in SymCrypt (the crypto library used by Windows and Azure) using safe Rust and performed formal verification using the Lean framework.
- Method: The Aeneas tool is used to translate Rust code into pure Lean models to prove compliance with standard specifications. AI agents were introduced to write independently verifiable proofs, thereby scaling automation.
- Progress: A code branch containing complete proofs for SHA-3 and ML-KEM (post-quantum cryptography) has been open-sourced, with ongoing expansions to more algorithms like AES-GCM.
- Advantage: Software engineers can continue writing high-performance Rust code while verification engineers work on the generated Lean models without interfering with each other.
More from coding & agent
- Biotech Agent Series Day 8: A Notebook Review Agent to Auto-Audit Lab Records — nlarusstone · 2026-10-27
- Photon Launches Agent-to-Agent Messaging in iMessage for Real AI Collaboration — alvelda · 2026-10-27
- Fake-paper meme shows an agent workflow for reverse engineering trading systems into a one-person quant fund — PtrPomorski · 2026-10-27
- Codex clones Linear's core from a one-page spec in 3 minutes 28 seconds — aakashgupta · 2026-10-27
- Reticle builds a verification layer that lets AI coding agents check their own generated code — Scobleizer · 2026-10-27
- Trust your agent, but read its logs: Claude managed agents tips — brada · 2026-10-27