Loading…
7-9 October, 2026
Prague, Czechia
View More Details & Registration
Important Note: Timing of sessions and room locations are subject to change.

The Sched app allows you to build your schedule but is not a substitute for your event registration. You must be registered for Open Source Summit Europe 2026 to participate in the sessions. If you have not registered but would like to join us, please go to the event registration page to purchase a registration.
← Back to schedule
TLA+ in the Age of AI-Assisted Engineering - Igor Konnov & Thomas Pani, Independent
Friday October 9, 2026 16:30 - 17:10 CEST
Club A (Floor 1)
Over several decades, TLA+ has been immensely useful for finding safety and liveness issues in concurrent and distributed systems. As developers of Apalache, the symbolic model checker for TLA+, our work with engineers has changed how we think specification tooling should look. Three obstacles to adoption arise repeatedly: (1) the steep learning curve, (2) the gap between formal specs and the code, and (3) scalability issues.

This talk reflects on our 10 year journey with TLA+ into the age of AI. We first show how we addressed (1) through a less mathematical syntax and modern developer experience. For (2) and (3), model-based testing and proofs have long been promising, but traditionally required too much expert labor. Frontier AI tooling changes this balance: it lowers onboarding costs, helps generate test drivers, and can automate proof work to a useful degree.

At the same time, formal tooling allows us to gate AI-generated code, catching plausible but incorrect implementations. We argue that AI and formal tooling complement each other, making both more practical.
Speakers
avatar for Igor Konnov

Igor Konnov

Independent Researcher in Formal Verification and Security
Igor Konnov is an independent security and formal methods researcher, practicing formal verification, differential testing, and fuzzing of distributed protocols. He is the principal maintainer of Apalache, a symbolic model checker for TLA+, under the Linux Foundation and TLA+ Fou... Read More →
avatar for Thomas Pani

Thomas Pani

Independent Consultant, Specification and Reliability Tools
Thomas Pani is an open source developer working on specification languages, developer tooling around executable specifications, and high-assurance distributed systems. He is a maintainer of Apalache, a symbolic model checker for TLA+, and an early contributor to Quint, a modern specification... Read More →
Friday October 9, 2026 16:30 - 17:10 CEST
Club A (Floor 1)
  Safety-Critical Software

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Tweet Share

Get help with the event

Contact event planner Event login
View support guides Find upcoming events
Create an event you'd love to attend!
Explore why organizers choose Sched • Success stories
Event App • Event scheduling • Event registration • Event ticketing • Sched forms • Call for papers • Badges • Conferences
© 2026. SCHED LLC - All rights reserved - Helping events since 2008
Event Planning App • Privacy • Terms
Share Modal

Share this link via

Or copy link