Liqi Geng

> Is there an existing flexible raft tla+ specification? Yes. https://github.com/fpaxos/raft.tla

I think we should also consider the entries in `AppendEntries` msg. They can be fetched asynchronously too.

> Case 2 can happen. How about only updating `committed_index` when `matched` is also updated for leader? /cc @gengliqi Looks good to me.

I think maybe we don't need to maintain this invariant. Though it may make users a little bit confused.

> https://zhuanlan.zhihu.com/p/228335745 may be helpful which provides a TLA+ formal verification, as well as a detailed explanation for the original algorithm. I have seen it yesterday. What a coincidence！🤣

Does the `store-io-pool-size` change to a non-zero value when testing? #11147 should not take effect if `store-io-pool-size` is 0 by default.

I think it's not a problem because this operation should be forbidden. The remove-single-voter configuration change relies on the condition that the number of Cnew voters must be greater than...

It's the same as https://github.com/tikv/tikv/issues/8381, I think we must add some check before proposing `conf change` to forbid promoting an uninitialized learner to voter. /cc @NingLin-P

> > It's the same as #8381, I think we must add some check before proposing `conf change` to forbid promoting an uninitialized learner to voter. /cc @NingLin-P > >...

> Have you decided the release for this feature ? Not yet. There is a lot of correctness-related work needs to be done because this optimization will change the fundamental...