I can confirm the issues with formal methods. I was working on a new type of locking mechanism and thought I would be smart by modelling it in spin [http://spi

I can confirm the issues with formal methods. I was working on a new type of locking mechanism and thought I would be smart by modelling it in spin [http://spinroot.com http://spinroot.com], which has been used for these kind of things before. I ended up with a model that was proven in spin, but still failed in real code. Given that's anecdata with a sample size of 1, but still was a valuable experience to me.