Currently stuck between a rock and a hard place with things like this.
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's still very familiar. Though things like SMACK and DiVinE are helping to decrease the gap between spec and code.
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's typical problem domain, being fairly limited in types of languages supported for extraction, and/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.
The good news though is that there'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's truly wonderful.
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's still very familiar. Though things like SMACK and DiVinE are helping to decrease the gap between spec and code.
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's typical problem domain, being fairly limited in types of languages supported for extraction, and/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.
The good news though is that there'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's truly wonderful.