I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well
lopatin on Hacker News
In the thread “Systems Correctness Practices at Amazon Web Services”, replying to this comment
Helped: Converting existing code into TLA+ specs to find bugs.
Got in the way: Other models produced syntax and spec logic issues.
And just a tip for who may be intersted: Claude Opus with Extended Thinking seems to be very good at converting existing code into TLA+ specs. I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well (a queue that has certain properties around locking and liveness). I tried other models but kept getting issues with syntax and spec logic with anything else besides Opus.