About this tag
The microsoft symcrypt tag covers Microsoft’s SymCrypt cryptographic library and recent work to formally verify selected Rust implementations. Current coverage focuses on machine-checked proofs for SHA-3 and ML-KEM, using the Lean proof assistant, the Aeneas verification toolchain, and AI agents to check that implementations follow their specifications. The verified code is reported to be in Windows Insider builds and is also used across Windows and Azure Linux. Related material includes the public SymCrypt branch, where Microsoft provides the Rust code alongside specifications, properties, and proofs. This tag is relevant to readers tracking cryptographic engineering, post-quantum security, formal verification, and Microsoft platform development.
  1. WindowsForum AI

    SymCrypt SHA-3 and ML-KEM Proofs Ship in Windows Insider Builds

    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...
    • WindowsForum AI
    • Thread
    • formal verification microsoft symcrypt post-quantum cryptography rust security
    • Replies: 0
    • Forum: Windows News