Bacelar Almeida, J., Barbosa, M., Barthe, G., Grégoire, B., Laporte, V., Léchenet, J.-C., … Strub, P.-Y. (2023). Formally verifying Kyber: Episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2023(3), 164–193. https://doi.org/10.46586/tches.v2023.i3.164-193