I keep posting this but it keeps being relevant. I had an agent implement a feature completely backwards. It wrote a whole bunch of tests proving the correctness of the implementation. All the tests passed.
The really interesting thing to me is that formal verification wouldn't have helped there either -- it would have just written a mathematical proof of the correctness of the backwards feature.
The really interesting thing to me is that formal verification wouldn't have helped there either -- it would have just written a mathematical proof of the correctness of the backwards feature.