Bacelar Almeida, J.; Barbosa, M.; Barthe, G.; Grégoire, B.; Laporte, V.; Léchenet, J.-C.; Oliveira, T.; Pacheco, H.; Quaresma, M.; Schwabe, P. Formally Verifying Kyber: Episode IV: Implementation Correctness. TCHES 2023, 2023, 164-193.