@article{ ABB+23,
  author        = {Jos{\'e} Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Benjamin Gr{\'e}goire and Vincent Laporte and Jean-Christophe L{\'e}chenet and 
                   Tiago Oliveira and Hugo Pacheco and Miguel Quaresma and Peter Schwabe and Antoine S{\'e}r{\'e} and Pierre-Yves Strub},
  title         = {Formally verifying Kyber -- Episode IV: Implementation Correctness},
  journal       = {Transactions on Cryptographic Hardware and Embedded Systems},
  publisher     = {Ruhr University Bochum},
  issue         = {2023-3},
  year          = {2023},
  pages         = {164--193},
  note          = {\url{http://cryptojedi.org/papers/\#hakyber}},
}