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

- Company: Microsoft Research (microsoft.com)
- Announced: 2026-07-13T16:00:00+00:00
- Subject: Research / Phi
- Source: https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/
- Record: https://forck.live/items/2458-verifying-rust-cryptography-in-symcrypt-from-standards-to-code

Microsoft Research announces the release of formally verified cryptographic code in SymCrypt, using Rust, Lean, Aeneas, and AI agents for proof automation, initially for SHA-3 and ML-KEM.

## Evidence

Verbatim from https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/:

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

---

Record: https://forck.live/items/2458-verifying-rust-cryptography-in-symcrypt-from-standards-to-code
Catalogue: https://forck.live/llms.txt
Feed: https://forck.live/feed.md