Tbh while DST (or just "testing" as hardware people would call it) is very obviously a great idea, I'm not sure it would have helped here - in order to detect these TOCTOU bugs you would need stimulus that triggers it and some kind of checker/model that has the correct behaviour.

That's totally possible but it's pretty hardcore testing for a software project and it's difficult to imagine doing that without realising that you have a TOCTOU issue just by inspection.