Bacelar Almeida, J.; Barbosa, M.; Barthe, G.; Grégoire, B.; Laporte, V.; Léchenet, J.-C.; Oliveira, T.; Pacheco, H.; Quaresma, M.; Schwabe, P.; Séré, A.; Strub, P.-Y. Formally Verifying Kyber: Episode IV: Implementation Correctness. TCHES 2023, 2023 (3), 164-193. https://doi.org/10.46586/tches.v2023.i3.164-193.