--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2020 ---
Hello Matthias, As Patrick pointed out, âACSL by Exampleâ contains several dozens of lemmas that were proven with Coq. https://github.com/fraunhoferfokus/acsl-by-example They are contained in the file https://github.com/fraunhoferfokus/acsl-by-example/blob/master/StandardAlgorithms/wp0.script However, our PDF does NOT explain how to use, let alone how to learn Coq. https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf