--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2020 ---
Hi Jens, thank you for your answer, ACSL by example is an excellent resource. > 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 ! I fully agree with you. My goal is to refine lemmas in such a way that the automatic provers are sufficient. My knowledge in Coq is still quite basic, but here my question really is about how to use Frama-C / Coq in combination. It seems to be in transition away from the native interface and the examples I found all use native:coq or even now completely removed options like `-wp-proof`. Best regards Matthias