I second the proposal. 1. As an aside, would we be open to accept other alternative forms of proofs such as property based testing (semi-formal methods) in future?
2. TLA+ serves as a proof of correctness for the specification. The north star would be to have assertions for invariants defined in TLA+ in our integration tests so that we can also have proof of correctness for the implementation. Do you have any thoughts on this? -- Divij Vaidya On Tue, Jul 26, 2022 at 5:21 PM Haruki Okada <ocadar...@gmail.com> wrote: > Hi. > > That also sounds good to me. > > TLA+ spec helps us to understand the protocol from a high-level. > Also I agree with Tim's point that the spread of familiarity with > formal methods would be beneficial in the long term. > > 2022年7月26日(火) 23:58 Tom Bentley <tbent...@redhat.com>: > > > 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 > > > > > -- > ======================== > Okada Haruki > ocadar...@gmail.com > ======================== >
