This is a very nice bug that I stumbled into while running the great auto_test tool on some code I had written. It is a beautiful example of a bug, because it is a very small bug that is still nearly undetectable for the average developer. Also, I do not know about any formal verification tool that could reveal the bug.