Hacker News new | ask | show | jobs
by harryfyx 1017 days ago
Raft has a TLA+ proof, which should make it "bug free". I understand your post is a joke, but I wonder if there are actually any errors.
1 comments

Actually, AFAIU the TLA+ proof is only for a few small cluster sizes - not for all sizes. And the number of nodes in the painting is definitely above that checked by TLA+...