Nieuws

Microsoft bewijst correctheid van Rust-cryptografie in SymCrypt met behulp van AI-agents

Microsoft heeft formele verificatie toegepast op cryptografische algoritmen in Rust, geschreven voor SymCrypt, met behulp van de Lean-proefassistent en Aeneas. AI-agents schrijven en onderhouden de bewijzen om de verificatie schaalbaar te maken. De eerste release bevat geverifieerde code voor SHA-3 en ML-KEM, die al in Windows preview-builds wordt gebruikt.