Formally verifying Kyber: Episode IV: Implementation correctness. TCHES. 2023;2023(3):164-193. doi:10.46586/tches.v2023.i3.164-193