The Correctness of a Code Generator for a Functional Language. - Nathanaël Courant; Antoine Séré; Natarajan Shankar (VMCAI, 2020)

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)

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)