A. Jesse Jiryu Davis
- Current and Future Tools for Interactive TLA+
A talk I gave at the 2021 TLA+ conference with Samy Lanka.
- Two attempts to compare a TLA+ spec with a C++ implementation
At MongoDB we tried two methods to test that a spec matches the code: one worked, one didn't. We explain our results in a VLDB 2020 paper.