A. Jesse Jiryu Davis
- Intro to TLA+ for the LLM Era: Prompt Your Way to Victory
You can go far without writing TLA+ syntax now, but you still need to understand temporal logic.
- Review: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
Some TLA+ experts try to teach LLMs to write TLA+. The LLMs fail.
- Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs
Five years ago we tried to test conformance, and only half-succeeded. Here's what happened, and the view from 2025.
- Are We Serious About Using TLA+ For Statistical Properties?
Should the temporal logic of actions also do performance modeling?
- Jesse's 2025 TLA+ Community Event Notes
A one-day conference about temporal logic.
- 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.