Paper 2023/010

Verifying Classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation

Martin Brain, City, University of London
Carlos Cid, Simula UiB, Okinawa Institute of Science and Technology Graduate University
Rachel Player, Royal Holloway University of London
Wrenna Robson, Royal Holloway University of London

Developers of computer-aided cryptographic tools are optimistic that formal methods will become a vital part of developing new cryptographic systems. We study the use of such tools to specify and verify the implementation of Classic McEliece, one of the code-based cryptography candidates in the fourth round of the NIST Post-Quantum standardisation Process. From our case study we draw conclusions about the practical applicability of these methods to the development of novel cryptography.

Note: Acknowledgement of EPRSC and UK Government funding added.

Available format(s)
Publication info
Published elsewhere. Minor revision. CBCrypto 2022
computer-aided cryptographypost-quantum cryptographyformal methodsverification
Contact author(s)
martin brain @ city ac uk
carlos cid @ oist jp
rachel player @ rhul ac uk
wrenna robson 2019 @ live rhul ac uk
2023-11-16: revised
2023-01-03: received
See all versions
Short URL
Creative Commons Attribution


      author = {Martin Brain and Carlos Cid and Rachel Player and Wrenna Robson},
      title = {Verifying Classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation},
      howpublished = {Cryptology ePrint Archive, Paper 2023/010},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.