I would encourage everyone to try this on some self-contained, state-machine like problems, if they have them. At my company, some experts were optimizing our clustering and failover logic by adding a bit more state (and hence complexity). Despite me not being an expert in that area, I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem. It was a bug that was not possible in the prior implementation of the system and no one thought to write unit tests for the sequence of steps that triggers it, so initially went unnoticed. The only thing that caught it was the TLA+ invariants, which, yes, were written by Opus as well.
As a side note, there's a lot of talk about programming being not fulfilling anymore. But the above exercise was probably the most fun I've had with engineering in a long time, and would have been nearly impossible for me personally without AI. Perhaps it was the novelty of the TLA+ stuff, but I think it offers a glimpse into what our jobs could actually be in the future, beyond simply telling Claude to do what you used to do manually and then clicking enter. There are much more ambitious and fulfilling use cases for it.
I had a similar experience having Astra add TLA+ and Lean verification tests to a project with somewhat complex state and many small algorithms (almost all generated by coding agents). The system had been working quite well, but adding formal verification surfaced 33 classes of bugs, some of which had several instances.
I completely agree with you about how fun these things can be. I've long believed in automated testing methods that were beyond what I could justify. I learned about formal methods in college in the 1980s and have never been able to justify (even to myself) applying them. Now a volunteer project I've been working on has 100% standard test coverage, many property-based tests, and 1000s of formal verification tests. That combination has surfaced multiple bugs in widely used underlying libraries and a bug in Rosetta 2's Intel emulation that was affecting me. And that's all just on the testing front. I'm having a lot of fun with all this.
lopatin · · focus · HN ↗
As a side note, there's a lot of talk about programming being not fulfilling anymore. But the above exercise was probably the most fun I've had with engineering in a long time, and would have been nearly impossible for me personally without AI. Perhaps it was the novelty of the TLA+ stuff, but I think it offers a glimpse into what our jobs could actually be in the future, beyond simply telling Claude to do what you used to do manually and then clicking enter. There are much more ambitious and fulfilling use cases for it.
rented_mule · · focus · HN ↗
I completely agree with you about how fun these things can be. I've long believed in automated testing methods that were beyond what I could justify. I learned about formal methods in college in the 1980s and have never been able to justify (even to myself) applying them. Now a volunteer project I've been working on has 100% standard test coverage, many property-based tests, and 1000s of formal verification tests. That combination has surfaced multiple bugs in widely used underlying libraries and a bug in Rosetta 2's Intel emulation that was affecting me. And that's all just on the testing front. I'm having a lot of fun with all this.