TLA+ has shown good promise in verifying cache-coherence protocols in multicore systems (a good alternative to CMurphi). An intern an Microsoft one helped uncover a bug in the Xbox 360, right before its 2004 launch - by formally verifying the protocol.

A few serious RISC-V startups use it today as well..