Do you (or people you know?) plan on publishing peer reviewed papers for how the lease algorithm works, how the multi-version concurrency control model works (and so on)?

None of these are afaik things built in to raft but are add-ons that etcd has created (that may or may not even use raft).

It'd be great to instill confidence in these add-on features by having them peer-reviewed in a similar manner as raft is/was/has been.

Raft - cool!

I'm aware that implementations diverge or do not directly synthesize from their specifications. At least not yet.

I'll be poking around more to see if the etcd team has published their own specs for the novel parts of the system. I'm particularly interested in seeing if/how OSS projects are adopting more rigorous "engineering" practices.

I took a look at the etcdv3 raft.go code, it is indeed pretty nicely written! Definitely better than any other one i've seen.

(though i'm pretty excited about the raft impl my summer intern and I are hacking on currently :) )

In Haskell, I presume? Will it be open sourced? :)

Actually doing in Agda first. Coinductive programming is a delight with Agda 2.5.

But yes that's the plan.

Consul's Raft implementation is leagues better than etcd's, unfortunately.

I'd be very interesting in hearing more about this.

I tried using both the Consul and etcd Raft implementations as libraries. I found the Consul library much easier to interface with. But it was my impression that the etcd library was much more tested in the real-world, with big projects like Kubernetes and with the library being embedded into projects like CockroachDB. I also wasn't sure if the details that the Consul implementation was hiding were actually important.

Is that still the case with Etcd v3? I remember reading somewhere that they were rewriting the Raft implementation in Etcd a good while ago.