I have written the second iteration of the TLA+ specification which now includes:

• The AddPartitionsToTxn request/response.

• Transaction coordinator (TC) elections so that leadership of a transaction log partition can now move between brokers.

• Producer fencing and some of the abort transaction logic.

I have written a Fizzbee spec that is the equivalent of the TLA+ spec.

Let’s dive into the decisions I had to make with this initial Fizzbee spec.

One thing I forgot to write about yesterday was how I get confidence that the TLA+ specification is doing what I expect. The thing about model checking a spec is that because there are usually millions or billions of states to explore, you can’t always see that certain states that should be reachable do get reached. It’s common to have a specification bug that causes your spec to have valid areas of the state space be unreachable, without you knowing it. This is why TLA+ practitioners learn to be a skeptical bunch and treat early success with great cynicism.

This is what I did to get confidence in this initial specification.

Strap in and fire up your nerd engines—this one's gonna be intense!

In my previous diary entry, I explained I would begin the formal modelling of Kafka transactions by implementing a tiny initial piece of the protocol - how a producer obtains a producer id. In this post I will discuss some aspects of the TLA+ specification I have written of this initial model.

A few days ago I started my work of formally verifying Apache Kafka transactions in both TLA+ and Fizzbee. I’ve decided to write a kind of diary of my progress so that others who are interested in formal verification of complex systems can read along and see how I go about it.