imho, model checker suits for the problem with many different states and complex state transformation.
But in this case, it's a simple toctou problem.. Using model checker sounds weird for me
If you added model checking to it you could have prevented it though, because people that know how to program a model checking program, will see the error right away.