Oh! I didn't expect this to show up here! Happy to answer questions, if folks have any. While this is on frontpage, I'd like to ask: if anyone has experience w

Oh! I didn't expect this to show up here! Happy to answer questions, if folks have any. While this is on frontpage, I'd like to ask: if anyone has experience with machine proofs, I'd appreciate your help in completing a formal proof of Elle's correctness. I've been teaching myself Isabelle/HOL in an attempt to formalize the proof sketch, and I have encoded most of the formalism and properties I care about, but actually proving lemmata has been... frustrating. Like, I burned hours one one lemma because it hinged on showing \forall x :: Nat, x \in N. https://github.com/jepsen-io/elle/tree/master/proof https://github.com/jepsen-io/elle/tree/master/proof If you'd like to work on this, my email is aphyr@jepsen.io!