Bacelar Almeida, J. (2023) “Formally verifying Kyber: Episode IV: Implementation correctness”, IACR Transactions on Cryptographic Hardware and Embedded Systems, 2023(3), pp. 164–193. doi: 10.46586/tches.v2023.i3.164-193.