On the Promises of ‘High-Assurance’ Cryptography
Summary
Symbolic Software analyzes Cryspen's high-assurance cryptography claims, detailing four new issues in libcrux and the lack of public disclosure. The piece argues that formal verification focuses on a narrow model, while platform-specific bugs and specification violations remain unaddressed, calling for more transparent security practices.