As asked in the question, this post asks the topicallity of "formal verification" tools.

I realize I have little experience with "formal verification" and I don't fully grasp its concepts. I saw this the phrase "verifcation tool(s)" from the round-3 official comment of NTRU Prime reacheable from here, and I assume it's some kind of formal tools or methods.

This question asks

Q1: are questions asking for tools for "formal verification" on-topic?

Q2: if on-topic, how should we define the scope for "formal verification" tools?

  • $\begingroup$ I read this and I didn't immediately have an answer, after which it got to the back of my mind. I'll raise it in the mod chat too. Sorry about the delay. $\endgroup$
    – Maarten Bodewes Mod
    Sep 30, 2021 at 22:53

1 Answer 1


Formal verification tools cover a wide range of topics.

I think that there is some very interesting work being done with protocol verification tools such as CryptoVerif, EasyCrypt, ProVerif and Tamarin Prover. I’d consider these very on topic.

The next closest to our bailiwick is probably tools to validate implementation. Cryptography specific tools such as Cryptol probably still count, but queries on generic software assurance tools should probably go elsewhere.

The relative merits of the on-topic tools would still be opinion-based and that aspect would still need to be moderated.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .