> Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processe

> Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow. Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful. > I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all. 'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this: > 1. Suppose we have a document with version 57 > 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59. > 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id. Which was a bug TLA+ found in ElasticSearch.[2] [1]: https://dl.acm.org/doi/10.5555/1779934.1779955 https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...