Most state-based formal methods, like B, Event-B or Z, provide support for static typing.

The ProB disprover uses constraint solving to try and find counter examples to proof obligations.

In a previous work, we applied constraint solving techniques to problems like invariant preservation and deadlock freedom checking.