DEV Community: Federico Ponzi

GenAI-accelerated TLA+ challenge

Federico Ponzi — Tue, 06 May 2025 17:26:41 +0000

Sharing this news here hoping you might find it interesting!

TLDR; if you have some experience with LLMs and TLA+, there is a chance to win some prizes. If you have experience with LLMs but not with TLA+ yet, but you are interested in developing TLA+ tools, apply to the TLA+ grant program.

The original announcement can be found on the TLA+ foundation website: https://foundation.tlapl.us/challenge/index.html

TLA+ is a formal specification language designed for modeling and verifying concurrent and distributed systems.

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:

Intelligent refactoring of TLA+ specifications (e.g., managing UNCHANGED correctly when adding variables)
LLM-enhanced linters, formatters, or other development tools
LLM-driven tools for automated grading in education
Visualizations of specifications or execution traces
Generation of type annotations for tools like Apalache
Synthesis of inductive invariant candidates, validated via TLC or Apalache
Synthesis of TLAPS proofs
Synthesis of entire specifications from source code and design documents

Evaluation

Submissions will be judged by the TLA+ Specification Language Committee (SLC)

The Jury will evaluate submissions based on their functionality, relevance to the TLA+ ecosystem, and the thoughtful use of AI. Submissions must be reproducible by the Jury. Passive formats, such as videos alone, are not sufficient. However, the Jury does not require a fully polished product—a prototype is sufficient. All submissions must be released under the MIT license, and any underlying AI models must be publicly available.

The use of GenAI/LLMs is explicitly encouraged, provided that any AI-generated content—such as specs, invariants, visualizations, … —is checked using some form of verification such as the TLA+ tools.

Catch the live announcement at the TLA+ Community Event 2025!

Participation Criteria

Eligible participants must meet the following:

Prior engagement with the TLA+ community (e.g., contribution to mailing lists, forums, open-source repositories, conference presentations, or academic publications)
Must not be a member of the TLA+ Foundation Board or Specification Language Committee
Must not be subject to any legal, contractual, export control, or jurisdictional restrictions that would preclude participation

Submission Timeline & Announcement

Submissions will open alongside this announcement. The deadline to submit entries for the challenge is two months from the announcement date on 07/03/2025. Submissions must be sent to genai@tlapl.us. The jury will select the winner one month after the submission period closes. We welcome innovative, technically robust, and practically valuable contributions that explore and expand the potential of GenAI within the context of TLA+.

For longer-term or foundational engineering and research efforts related to TLA+, we encourage you to explore the TLA+ grant program.

Distributed Snapshots: Chandy-Lamport protocol

Federico Ponzi — Fri, 31 May 2024 17:54:49 +0000

Some forms of distributed snapshots were around for a while already when Chandy-Lamport's distributed snapshots paper was first published in 1985. Lamport considers this protocol a straightforward application of the basic ideas from Lamport clocks. Other than reviewing the paper, in this post I'll also present some examples of real world implementations and a TLA+ specification of the protocol.
What problem is it trying to solve?

You need to record the global state of a program. Why? Because, for example, you have some complex computation ongoing, and you want to know which step has reached. Or you have a long-running computation, and you want to take a snapshot as a backup to allow restarting the computation again from the checkpoint rather than from the beginning in case any machine fails.

For the state of the program, we refer to the local variables and in general to the history of states that the program went through.

Why is taking snapshots hard? Well, first of all, the snapshotting algorithm should not interfere with the running computation.

Secondly, if your program is a single process on a single machine, this is straightforward! You could create an api to say "record the snapshot in 5 seconds" or "every 2 hours". For a multi-thread/multiprocess program running on a single machine, you can create a similar api.

In a distributed system, this api won't work because there is no global shared clock. You could end up with out-of-sync snapshots providing an inconsistent view of the system. Other than the state of the process itself, we could also have inflight messages that should be included in the snapshot. As an example of inconsistent snapshot, a process B could record that it received a message from A and A's snapshot does not include that the message was sent over to B.

The paper has a good visual representation: imagining you wanted to take a picture of a sky filled with migrating birds. One photo is not enough, you will need to take multiple pictures and stitch them together in a way that provides a consistent view of the landscape. This is the challenge that this paper is trying to solve.

TLA+ is easy if you know how to abstract

Federico Ponzi — Sun, 29 Oct 2023 11:19:21 +0000

I've been wanting to learn TLA+ for a while now, and I finally had a chance to do it thanks to a seminar series held by Professor Murat Demirbas. In this article, I will talk about my experience with formal methods and TLA+, and I will also share some of the things I've learnt that I think will be very useful when writing your specifications.

By the end of this article, I hope that you will:

Have a basic understanding of formal methods and model checking
Understand how TLA+ can improve algorithm and system design
Have some intuition on what it takes to write a spec in TLA+
Want to learn some TLA+.

As always, let's start with the problem we're trying to solve.
What problem do formal methods help solve?

English is considered a very ambiguous language. When we build a complex system, we need an unambiguous specification (also known as "spec"). Formal methods use math to define a rigorous system model. After we have written the code for the model, we can then also use it to verify some properties.

The benefits of formal methods are twofold:

Unambiguous specification of our systems and algorithms
Verification of properties for these models

An example of a property that can be verified is that no execution can result in a deadlock. This would be very difficult to prove in a test, especially if it spans multiple systems.

We can also verify that an algorithm is correct by writing some properties as invariants. An invariant is simply a predicate that should always hold true. Invariants are sometimes used in asserts.

We can define correctness and liveness properties. For example, we could verify that eventually some property will hold, such as that our new sorting algorithm eventually sorts its input.

Formal methods allow you to explore different designs and optimize performance while maintaining confidence that the system is doing the right thing.

Experiments with eBPF: Snitchrs

Federico Ponzi — Sun, 16 Jul 2023 20:23:20 +0000

In this post, I will share my experience on learning and playing with Extended Berkeley Packet Filter (eBPF). It's a very cool technology that not anyone might be aware of. It's been a while since I planned to learn some eBPF and this post has some good information for anyone who wants to get started. eBPF is a Linux kernel feature that allows to easily and safely interact with the kernel.

In order to learn how to use eBPF, I decided to implement Snitchrs a simple program that shows on a map to which IPs your computer is connecting to.

I will go through interesting snippets of code I had to write in order to implement this program. This article is not meant to be a tutorial but rather an explanation that will hopefully help you better understand useful things to know in order to write your own eBPF programs. I'll assume some basic knowledge of the TCP/IP stack and how the Linux kernel works.

Continue reading... but feel free to leave comments here!