Sisyphus - Mostly Automated Proof Repair

1 min read Original article ↗

1

Scalable

We evaluated Sisyphus on 14 OCaml programs, 10 of which were taken from real-world OCaml libraries (Jane Street's Core, Inria's Menhir, Containers e.t.c.).

2

Elegant

Sisyphus's repair procedure builds some of the most elegant truths of Computer Science, the Curry-Howard correspondence, to automatically and efficiently infer invariants for programs.

3

Free

Sisyphus is built from the ground up using Free (as in freedom) technologies, and is licensed under the ultimate AGPLv3+ libre license to ensure the Freedoms of its users are preserved!