@misc{ BKL+25,
  author        = {Manuel Barbosa and Matthias J. Kannwischer and Thing-han Lim and Peter Schwabe and Pierre-Yves Strub},
  title         = {Formally Verified Correctness Bounds for Lattice-Based Cryptography},
  booktitle     = {Proceedings of the 2025 {ACM SIGSAC} Conference on Computer and Communications Security, {CCS'25}},
  publisher     = {ACM},
  pages         = {to appear},
  year          = {2025},
  note          = {\url{https://cryptojedi.org/papers/\#frodoec}},
}