Séminaire LSL - Virgile Prevosto - 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.

Acknowledgments

Joint work with Martin Hána, Nikolai Kosmatov and Julien Signoles, to be presented at AISoLA'26