If you're interested in building one and you have experience with them, get in touch and we can work through it together. I think the biggest challenge would be modeling the semantics of write concern, but I'm not that familiar with proof assistants, maybe that isn't too hard.
Amazon has used a TLA+ model for their distributed systems and found a bunch of bugs [2].
Seriously, everybody fucks this up. Please please learn a model checker and check your algorithm.
[1] In the "Summary of Jepsen Test Results" section: http://blog.foundationdb.com/call-me-maybe-foundationdb-vs-j...
[2] https://research.microsoft.com/en-us/um/people/lamport/tla/a...
See this to get yourself started: http://research.microsoft.com/en-us/um/people/lamport/tla/by...
Ark is just about making replication as a whole trustworthy. The jepsen post on MongoDB[2] shows MongoDB losing data even with majority write concern, which if used properly, is supposed to make MongoDB a CP system. But because of the design flaws in the election algorithm, you can't rely on it perfectly. The changes we made in Ark fix the election algorithm to make majority write concern actually able to guarantee data safety, so you can treat it as a fully CP system.
[1]: http://docs.tokutek.com/tokumx/tokumx-transactions.html
Then you need a formal model.
We have run Jepsen and have not been able to get it to show data loss in TokuMX. The problems it found in MongoDB were already fixed in other ways in earlier versions of TokuMX, but we're trying to get Jepsen to demonstrate the other problems we've found.
Model checking may be another way we can prove correctness, but since Ark is so similar to Raft, I think the Raft model in TLA+[1] is probably sufficient. Anyway, we'd also need a proof that the model is equivalent to the implementation, and I don't know of a way to do that, so I think functional tests are more important.
In any case, we'll look in to using a model checker, and any help would be greatly appreciated. If you're interested, feel free to email me.
The casual attitude that most people show when building these algorithms mind blowing.