[nine_k]

What kind of flaws? I would expect performance problems.

[jupp0r]

To start with, you usually perform verification on a behavioral model and not on the code itself. This opens up the possibility that there are behavioral differences between the code itself and the model which wouldn't be caught.

[nine_k]

Could you offer an example?

[jupp0r]

If you work through the TLA+ tutorial[1] it will help you get a good idea of the benefits and limitations of verification.

[1] https://learntla.com/