I'm +1 for inclusion in the main repo and I was going to suggest the same in the KIP-853 discussion. The original authors of 3 and 4 are part of the kafka community, so we can ask them to submit PRs.
Ismael On Tue, Jul 26, 2022 at 7:58 AM Tom Bentley <tbent...@redhat.com> wrote: > 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 >
