Comment by dgan

about a year ago, at my job, i wrote a spec for authentication in TLA+, and while writing it, i discovered a bug/attack vector, which would allow an attacker to basically bypass the double-authentication.

It surely did produce a fancy, mathy PDF which I proudly shown and explained to my team, but honestly, a little duck-talking would have permitted to find the same bug without TLA+

For aome context, it's a CRUD api + web interface for external clients, nothing too complicated, and I really wanted to try TLA+ in real life