--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on August 2020 ---
https://softwarefoundations.cis.upenn.edu/lf-current/index.html Once, you have wrapped your had around this introduction it should be much easier for your to write your own proofs for ACSL lemmas. One thing, I learned while working with WP is that not every lemma that cannot be verified at first really needs Coq. Sometimes, additional lemmas/assertions help in guiding the automatic provers. That being said, Coq is definitely worth learning ! Jens