From this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more).
Formal proof as in coq-proof are often not reasonable for many dynamic projects
Formal proof as in coq-proof are often not reasonable for many dynamic projects