“Formally verifying Kyber: Episode IV: Implementation correctness”, TCHES, vol. 2023, no. 3, pp. 164–193, Jun. 2023, doi: 10.46586/tches.v2023.i3.164-193.