Formosa-Crypto – Artifacts

• Formally verifying Kyber – Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt
• Formally verifying Kyber – Episode IV: Implementation Correctness
• Typing High-Speed Cryptography against Spectre v1
• High-assurance zeroization
• Protecting cryptographic code against Spectre-RSB
• Preservation of Speculative Constant-time by Compilation