Formally verifying Kyber Part I: Implementation Correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

Swoosh: Practical Lattice-Based Non-Interactive Key Exchange. - Phillip Gajland; Bor de Kock; Miguel Quaresma; Giulio Malavolta; Peter Schwabe (IACR Cryptol. ePrint Arch., 2023)

Formally verifying Kyber Episode IV: Implementation correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

SWOOSH: Efficient Lattice-Based Non-Interactive Key Exchange. - Phillip Gajland; Bor de Kock; Miguel Quaresma; Giulio Malavolta; Peter Schwabe (USENIX Security Symposium, 2024)

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. - José Bacelar Almeida; Santiago Arranz-Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Cameron Low; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 2024)