TLA+ Community Event 2026
Sunday, April 12, 2026
Torino, Italy
| time | title | speaker | affiliation | slides | recording |
|---|---|---|---|---|---|
| 09:00 | A Compositional Strategy for Verifying Fault-Tolerant Dynamic Task Graph Scheduling in Modern Cloud Environments | Quentin Delamea | Aneo & Univ. Saclay | ||
| 09:30 | A generic hardware in-order pipeline architecture model to capture key temporal properties | Mamoun Filali | CNRS & IRIT | ||
| 10:00 | Coffee Break | ||||
| 10:30 | Extensible Proof Decomposition Rules for TLAPS | Karolis Petrauskas | Vilnius University | ||
| 11:00 | Systematic API Testing through Model Checking and Executable Contracts | Ana Catarina Ribeiro | NOVA University, Lisbon | ||
| 11:30 | Model-based Testing of Practical Distributed Systems in Actor Model | Ilya Kokorin | ITMO University | ||
| 12:00 | Interactive symbolic testing with TLA+, Apalache, and LLMs | Igor Konnov | |||
| 12:30 | Lunch Break | ||||
| 14:00 | Thinking in TLA+ – Modeling Judgment for System Design | Murat Demirbas | MongoDB | ||
| 14:50 | P2P2P (PlusCal to PlantUML to PDF) | Jackson Belzer | Northern Arizona University | ||
| 15:20 | Towards Language Model Guided TLA+ Proof Automation | Yuhao Zhou | Northeastern University | ||
| 16:00 | Coffee Break | ||||
| 16:30 | Verifying differential privacy in TLA+ via self-products | Ugur Yavuz | Boston University | ||
| 17:00 | Veil: Multi-Modal Verification of Transition Systems | George Pîrlea | National University of Singapore | ||
| 17:30 | Roundtable & closing | ||||
| 19:30 | Workshop dinner |
Participants are required to register to ETAPS 2026 (early registration deadline: March 10, 2026). We encourage participants to include the workshop dinner on Sunday evening in their registration.
TLA+ is a language that is used in academia and industry for formally specifying systems. It is supported by verification tools, including the TLC and Apalache model checkers and the TLAPS proof system. PlusCal serves as a frontend for generating TLA+ specifications from an algorithmic language with an imperative flavor.
The TLA+ Community Event serves as a forum where practitioners and researchers interested in the use and further development of the TLA+ specification language and its tools meet and discuss.
Proposals for contributed talks are sollicited that present work of interest to users of TLA+ or PlusCal, such as:
There will not be formal proceedings, but the abstracts and presentations will be made available on the Web.
Proposed contributions should be submitted by January 31, 2026 to tla2026@inria.fr. It is expected that the contribution will be presented on 1-2 pages. Longer submissions will be read at the discretion of the program committee.