The Coq mailing list

[Stephan Merz <stephan.merz AT loria.fr>]

A short look at the GitHub repository seems to indicate that they moved to 
model checking. Although an interactive proof system for TLA+ does exist, I 
couldn't see any proofs in their modules.

Stephan

> On 18 Feb 2020, at 18:13, Fernandez, Matthew 
> <matthew.fernandez AT intel.com>
>  wrote:
> 
> Some of the Elasticsearch algorithms have been verified using TLA+ [0]. In 
> that repository is also a partial Isabelle formalization of the same. I had 
> a conversation with David Turner about why they moved away from Isabelle to 
> TLA+, but can't recall the exact details and motivation offhand. This might 
> be an interesting case study for you though, Talia.
> 
>  [0]: https://github.com/elastic/elasticsearch-formal-models
> 
>> -----Original Message-----
>> From: 
>> cl-isabelle-users-bounces AT lists.cam.ac.uk
>>  <cl-isabelle-users-
>> bounces AT lists.cam.ac.uk>
>>  On Behalf Of Talia Ringer
>> Sent: Saturday, February 15, 2020 17:27
>> To: Coq-Club 
>> <coq-club AT inria.fr>;
>>  isabelle-users 
>> <isabelle-users AT cl.cam.ac.uk>
>> Subject: [isabelle] Abandoned proof engineering efforts
>> 
>> 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