GenAI-accelerated TLA+ challenge

The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the GenAI-accelerated TLA+ challenge—an open call for submissions that explore the intersection of TLA+ and generative AI. This initiative aims to foster practical and innovative tooling, workflows, and approaches that bring the capabilities of generative AI and LLMs to TLA+. Participants are invited to develop engineering-oriented solutions that advance the usability, accessibility, and automation of formal specification through the integration of GenAI. Awards 1st Place: Nvidia GeForce RTX 5090 (sponsored by NVIDIA) 2nd Place: One-year single seat, individual subscription to Github Copilot Pro+ (sponsored by the TLA+ Foundation) 3rd Place: One-year single seat, individual subscription to Github Copilot Pro (sponsored by the TLA+ Foundation) Example Project Areas Participants may submit work including, but not limited to:

2025 - TLA+ Community Event :: TLA+ Community Event & Conference

lets-prove-blocking-queue/SPARK at master · lemmy/lets-prove-blocking-queue

Proving a blocking queue deadlock free in a dozen different ways - lemmy/lets-prove-blocking-queue

Supposedly deadlock-free version of blocking queue in Ada · Issue #2 · lemmy/lets-prove-blocking-queue

with Ada.Text_IO; use Ada.Text_IO; with Ada.Integer_Text_IO; use Ada.Integer_Text_IO; procedure blockingqueue is Buffer_Size : constant := 1; type Item_Array is array (1 .. Buffer_Size) of Integer;...

The TLA+ Home Page