Oh! I didn't expect this to show up here! Happy to answer questions, if folks have any.<p>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 <i>have</i> 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.<p><a href="https://github.com/jepsen-io/elle/tree/master/proof" rel="nofollow">https://github.com/jepsen-io/elle/tree/master/proof</a><p>If you'd like to work on this, my email is aphyr@jepsen.io!
This is really cool work, very exciting to see if published in paper form (I saw your talk about some of this last year)!<p>I had a question about your completeness argument (in 4.3.1), you say "we typically observe enough of a history to detect the presence of non-cycle anomalies". I think I understood why that is after reading the rest of the paper, but I didn't understand the worst case. Is it possible, for example, for a database to intentionally construct incorrect histories that Elle doesn't detect?<p>I don't have any real "evil database" threat model in mind, just trying to test my understanding.