CVN+MICS Seminar: Virgile Prevosto
Virgile Prevosto (CEA): From Manual to LLM-Assisted Formal Verification of a PKCS#1 Signature Parser
Abstract
Software engineering approaches assisted by Artificial Intelligence (AI) are receiving increasing attention. This work evaluates the ability of large language models (LLMs) to assist engineers in the formal verification process. We conduct an experiment using ChatGPT on a PKCS#1 (Public-Key Cryptography Standard) v1.5 signature parser that was recently (manually) specified in ACSL and verified with the Frama-C platform. Our approach prompts the LLM to generate ACSL annotations directly from the C code, cross-checks the generated specifications against known security requirements, and iteratively refines them to achieve a complete proof. In this verification loop, annotations are progressively improved using feedback from Frama-C. For failing proof obligations, we instruct the LLM to supply a sequence of ACSL assertions that guide the prover. Using structured prompts, we repeatedly obtain a complete proof for the target parser. This demonstrates that substantial parts of the formal verification workflow can be mechanized. We present our LLM-assisted verification approach, report its benefits and limitations, and compare it with the prior manual proof in terms of specification auditability and human effort.
This is a joint work with Martin Hána, Nikolai Kosmatov and Julien Signoles, presented at AISoLA'26 in October.
Biography
Virgile Prevosto is a CEA fellow. He carries his research in the Software Safety and Security Lab of the CEA List institute in Paris-Saclay (France). He is one of the lead developers of the Frama-C software analysis platform and his work focuses on formal specification and verification of software.
