[krenoten]

SPIN is a nice tool for modeling them. You can extract code from a coq model. You can go into the world of dynamic instrumentation to try to verify invariants in implementations.