I had claude spend about 2 hours friday modeling one of our kubernetes operators in TLA, and it found 8 bugs, including 2 that could cause data loss, and one of the other bugs was one we had been trying to figure out why it was happening for literally months.