J. Bacelar Almeida, “Formally verifying Kyber: Episode IV: Implementation correctness”, TCHES, vol. 2023, no. 3, pp. 164–193, Jun. 2023.