Bacelar Almeida, J. et al. 2023. Formally verifying Kyber: Episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded Systems. 2023, 3 (Jun. 2023), 164–193. DOI:https://doi.org/10.46586/tches.v2023.i3.164-193.