So, the simulator only works if it knows what "correct" looks like and what kinds of failures to throw at the code, right? Who decided those two things? Was it the same agent that wrote the code? Were those human-written, or did they fall out of the formal specs?
You had three things that could each say "this is right", the end-to-end tests, the formal model, and how the old Go version behaved. When they disagreed, which one did you trust? Did the test ever turn out to be the thing that was wrong?
When the simulator caught something before release, was it usually the code that was wrong, or the definition of correct?
Feels like there's some really useful insights about best practices for coding with agents. I wonder if the Bun team used a similar approach if they still would have switched.