| 08:55 | Welcome & Opening Announcements | | | |
| 09:00 | Keynote: Formal Methods at Microsoft | Nikolaj Bjørner | pdf | video |
| 10:00 | TLA+ for Nike Stores | Nathan Fairhurst | | |
| 11:00 | Specifying and checking an extension of Tendermint consensus in TLA+ | Jure Kukovec, Daniel Cason, Igor Konnov, and Josef Widder | pdf | video |
| 12:00 | Lunch | | | |
| 13:00 | Building Correct Distributed Systems with the PGo Compiler | Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do, Ruchit Palrecha, Yennis Ye, and Ivan Beschastnikh | pdf | video |
| 14:00 | Obtaining Statistical Properties via TLC Simulation | Jack Vanlightly and Markus A. Kuppe | pdf | video |
| 15:00 | Coffee Break | | | |
| 15:30 | Extending Apalache to Symbolically Reason about Temporal Properties of TLA+ | Philip Offtermatt, Jure Kukovec, and Igor Konnov | pdf | video |
| 16:30 | reTLA: Towards an automatic transpiler from TLA+ to VMT | Jure Kukovec, Aman Goel, Igor Konnov, Stephan Merz, and Karem Sakallah | pdf | video |
| 17:30 | End of the conference | | | |