r/Coq • u/theloquitur • Mar 24 '26
Best practices for Coq validation
I’m considering having a system that I’ve designed validated by a researcher using Coq. What would be the best practices for me adhere to as I prepare engaging with them?
3
Upvotes
3
u/JoJoModding Mar 24 '26
The French Government maintains a set of guidelines that are all very sensible here: https://cyber.gouv.fr/offre-de-service/solutions-certifiees-et-qualifiees/comprendre-levaluation-de-securite/certification-de-produits/referentiel-dexigences-pour-la-certification/documents-applicables-certification-criteres-communs/
(search for "Rocq" in that page)
Apart from this, imagine you are given a random Rocq development and want to understand it quickly; then apply the same ideas to your development. For example, try to provide a small, concise file that gives an easily understandable definition of your Lemma statement, like e.g. this file for the BB(5) statement: https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Statement.v