--- layout: fc_discuss_archives title: Message 82 from Frama-C-discuss on May 2010 ---
On Thu, 2010-05-20 at 13:44 +0200, Claude Marche wrote: > The lemma itself is not proved of course, you have to convince yourself > of its truth by other means: from human review to use of a proof assistant. Does that mean that Jessie/why doesn't prove a user supplied lemma? The ACSL reference is unclear on this, it states "Of course, a complete verification of an ACSL specification has to provide a proof for each lemma." It's unclear to me who has to provide this proof.