A friend of mine did an experiment with his grad students in his Formal Methods class. They all submitted their implementation of binary search and he modelled

A friend of mine did an experiment with his grad students in his Formal Methods class. They all submitted their implementation of binary search and he modelled them each in TLA+. The majority of them all had errors.