Earlier quoted context omitted.
You shouldn't have been able to formally verify the algorithm fails to protect the critical section. Wrapping ticket numbers can lead to starvation (literally, if we follow the baker analogy), but the algorithm protects the critical section so long as thread IDs are unique. The sort of environments in which this is a problem would be extremely uncommon. For a start, you need continuous contention. If you ever get a b…
I'm quite certain I formally verified that two processes were both able to get into the critical section WITH THE ALGORITHM I WAS VERIFYING, but this was 35 years ago, so details are fuzzy. Remember that this is long before Wikipedia and even before Google, so I have no idea where I'd have gotten the alleged Baker's algorithm from. Also you're right that this isn't much of an issue in practice , but that's not what f…
Formal verification at the undergraduate level, if you even see it, would be about running software on a spherical cow, though.