It really shines in protocol design, see [1] and [2] (both very recent posts). But you can use it for anything you are not confident enough about being correct. This happens very often when working with distributed systems, where there are way too many factors to consider.

More generally, TLA+ (the base language for Quint - Quint can transpile to TLA+) was used at AWS to find bugs and make aggressive optimizations in several services [3].

[1]: https://protocols-made-fun.com/consensus/matterlabs/quint/sp... [2]: https://informal.systems/blog/interchain-meet-starknet [3]: https://lamport.azurewebsites.net/tla/formal-methods-amazon....