Hi, I noticed that TLA+ has featured in the Test Plans of a couple of recent KIPs [1,2]. This is a good thing in my opinion. I'm aware that TLA+ has been used in the past to prove properties of various parts of the Kafka protocol [3,4].
The point I wanted to raise is that I think it would be beneficial to the community if these models could be part of the main Kafka repo. That way there are fewer hurdles to their discoverability and it makes it easier for people to compare the implementation with the spec. Spreading familiarity with TLA+ within the community is also a potential side-benefit. I notice that the specs in [4] are MIT-licensed, but according to the Apache 3rd party license policy [5] it should be OK to include. Thoughts? Kind regards, Tom [1]: https://cwiki.apache.org/confluence/display/KAFKA/KIP-848%3A+The+Next+Generation+of+the+Consumer+Rebalance+Protocol#KIP848:TheNextGenerationoftheConsumerRebalanceProtocol-TestPlan [2]: https://cwiki.apache.org/confluence/display/KAFKA/KIP-853%3A+KRaft+Voter+Changes#KIP853:KRaftVoterChanges-TestPlan [3]: https://github.com/hachikuji/kafka-specification [4]: https://github.com/Vanlightly/raft-tlaplus/tree/main/specifications/pull-raft [5]: https://www.apache.org/legal/resolved.html
