Microsoft выложила формальные верификационные доказательства для SymCrypt на Rust: ML-KEM и SHA3 под Lean
Microsoft открыла исходный код формальных доказательств корректности для криптографической библиотеки SymCrypt. Первый релиз включает полные верифицированные реализации ML-KEM и SHA3...
