--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2020 ---
Hello, I am looking at the WP plugin to prove lemmas for functions. In the case that the automatic provers do not manage to prove a PO, how does one proceed to get a script/.v file to be used in Coq to complete a proof externally? It seems that most what I found on this topic uses native Coq which is deprecated now. Maybe someone can point me to the current documentation for this. The WP manual presents tip for proof scripts but that seems to be for the interactive proof editor of the Frama-C GUI. Thank you for your help, Best regards Matthias