I was looking for what would amount to the world's simplest concurrent/distributed (i.e. multithreaded/multiprocess/network) design/architecture for which there was an implementation that satisfied the design but for which TLA+ is used to find a problem in the design. So it would be an end-to-end sort of look at a system that included TLA+ as a key artifact.
To my understanding, you're looking for a real-life example with specs and source code, where the bug was discovered via TLA+, right? There are a few things that make those finding resources tricky:
* Most people currently using TLA+ are using it for proprietary projects, so it's hard to find the spec or source code.
* Most people use TLA+ to either build new projects or changed known buggy ones, not necessarily to write specs looking for bugs in existing, "working" systems.
* Most TLA+ specs are for complicated projects.
Here's what I came up with.
This is an example of sample code where a bug was really hard to find with testing and really easy to find in TLA+, but it was a toy example for class. That said,
someone did run into an extremely similar bug in practice and provided code.
Here is a case of someone specifically using TLA+ to find a bug in an existing system, but he doesn't provide the full code.
Mongo wrote a simplified model of part of their database and found a bug that none of them knew about before; the code is available but very complex.
Does that help?
H