How to publish research accompanied by mechanically-checkable proofs

I've both written and reviewed research papers that incorporate mechanically-checked proofs (either as the main subject of the research or as supporting the correctness of other contributions).  Computer-aided formalization and proof are increasingly part of the mainstream of (the formal side of) programming languages research, and seem to be being especially enthusiastically adopted by students and junior researchers.  However, just having mechanically verified a proof of (some aspect of) a system is not enough - all of the standard considerations regarding the reporting of scientific research, on-paper proofs, or research code still apply. 

This post collects some guidelines that I hope will be helpful for researchers working on papers accompanied by formal proofs. I would have thought most of these were obvious, but have encountered enough counterexamples to disabuse me of this naive assumption.  The following is probably not an exhaustive list, but is offered as a starting point.


Read more »