TLA+ helped us fix and10 issues in our OSS project

Hi there!

A few weeks ago, Boris posted how formal verification helped fix issues in their codebase (https://x.com/bcherny/status/2102543349102338309) and I definitely wanted to try it out in the swarm codebase.

The idea was simple:

1. Go over the codebase and fine most critical parts that could be modelled 2. Pick the first few and try to model them based on main code 3. Find counterexamples 4. Generate failing tests for them (single tests file diff pr) 5. Go over each of them and fix them + add the counterexamples in the repo for reference

I think this pattern is super nice tbh, and it helps a lot on reasoning around the code and implementation, specially when AI was involved.

The main issue: we had to add a daily wf to check for any updates to the spec, so that we keep it in sync (price you pay when the language can not be expressive enough, e.g. js).

Another win was that for the heartbeat system, which I wanted to refactor for a while, it managed to propose a simplification from 1.3M states to only ~4k (lol).

I believe it can be used for complex systems refactoring, while keeping the same functionalities.

Blog post about it (beware AI generated, but it contains some of the prompts we used during the session, just point your agent to the link and let it cook) -> https://www.agent-swarm.dev/blog/tla-plus-races-agent-swarm

I've been wanting to use tla+ for years, but always struggled w the syntax when working on something non-trivial. AI generating the specs and explaining the reasoning behind them helped a lot!

If you curious about the specs -> https://github.com/desplega-ai/agent-swarm/blob/main/specs/t...

Cheers,