Verdi – Formally Verifying Distributed Systems (2016)
Currently stuck between a rock and a hard place with things like this.<p>Many of the other formal verification tools make it very easy to have your implementation drift or be entirely unmoored from your specification, but they let you keep working at a level of abstraction from your problem that&#x27;s still very familiar. Though things like SMACK and DiVinE are helping to decrease the gap between spec and code.<p>Using things like Coq + program extraction brings the overlap between spec and implementation into much, much closer alignment, but brings with it additional problems. Writing a complex program in a very abstract language further away from an engineer&#x27;s typical problem domain, being fairly limited in types of languages supported for extraction, and&#x2F;or still having to have an awful lot of faith in the extractor (which itself is unverified as near as I can tell) are all things that are currently keeping me out of Coq for immediate use cases.<p>The good news though is that there&#x27;s a lot of fairly high-profile work being done (like Verdi) to increasingly bring formal methods to increasingly complex software problems in ways that make using formal methods more approachable and usable, and that&#x27;s truly wonderful.