So much this.

I actually did take a formal verification course in college. Our final project was to use the techniques we'd been learning to verify some classic critical-section locking algorithm. I chose to verify an implementation of Lamport's bakery algorithm[0] in C (this was the 90s -- a lot of code was still being written in C).

The problem is that Lamport's algorithm makes an assumption that the "ticket number" is unbounded and any finite implementation in C will almost certainly use a value which is limited to 32 bits or so.

So I was able to formally verify that the algorithm fails to protect the critical section if enough processes are kept waiting to overflow the counter. :)

This probably just means that Lamport's algorithm isn't a great choice for such environments, but I'm still bummed that the professor gave me a B.

[0] https://en.wikipedia.org/wiki/Lamport%27s_bakery_algorithm