[andikleen3]

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], 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.