We've used it at various times to verify the design of some database kernel internals e.g. I/O scheduling. This is partly to give you confidence that the design is not broken, but on rare occasion it also surfaces design defects, like non-obvious race conditions.

Defects surfaced in the model may not imply defects in the software e.g. obscure race conditions in the model that cannot actually occur in implementation due to details not captured in the model. But it forces you to explicitly acknowledge and investigate that.