The Coq mailing list

[Christoph Sprenger <sprenger AT inf.ethz.ch>]

Dear Talia,

this is not my own proof effort, but I know Diego Ongaro formalized his Raft consensus protocol [1,3] in TLA and partially proved one of its properties in the TLA prover. He later abandoned the effort to prove further properties, since he “found it too tedious and time-consuming to use the TLA proof system at the scale of a complete proof” [2, Section 8.2], see also [1, Section 8.2].

Cheers, 

Christoph

—

[1] https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro

[2] https://web.stanford.edu/~ouster/cgi-bin/papers/OngaroPhD.pdf

[3] https://raft.github.io/

On 16 Feb 2020, at 20:18, Talia Ringer <tringer AT cs.washington.edu> wrote:

To clarify: any size project in any proof assistant is fine. I'd actually
really love examples of projects of different sizes in different proof
assistants. The more examples, the better.

On Sat, Feb 15, 2020, 5:27 PM Talia Ringer <tringer AT cs.washington.edu>
wrote:

Hi all,

I'm curious if any of you have ever started to verify a system, but then
abandoned that system due to the difficulty of evolving and maintaining
your proofs. If so, I would love for you to share those proof efforts with
me, especially if the code is public.

Thanks!

Talia