Automating Verification via LLM Agents

Research Intern: Katarzyna Biziel 

Project supervisor: Jianyi Cheng, Elizabeth Polgreen 

PhD Tutor: Leiqi Ye 

During my summer research internship, I investigated how Large Language Models (LLMs) can be used to automate formal verification of C programs using the bounded model checker, CBMC. The broader project aims to support the verification of C programs that are translated into Rust, but my work focused specifically on developing and evaluating the LLM-based verification pipeline.  

The pipeline I built asked an LLM to generate a postcondition for a given C function. The function, with the generated assertion inserted, was then passed to CBMC to determine whether the assertion could be verified. If verification failed, the resulting counterexample was fed back to the LLM, allowing it to iteratively refine its specification. 

While this initially appeared to be a relatively straightforward verification pipeline, developing a reliable approach revealed a much broader range of challenges beyond simply generating assertions. I investigated issues including bounded and unbounded loops, generating harnesses for library functions, handling syntactically invalid assertions, dealing with missing preconditions, as well as timeouts in the underlying SAT solver. A particularly important challenge was detecting vacuity, where an assertion could be technically verified but was trivially true for all inputs and therefore failed to provide meaningful verification. Testing the pipeline on increasingly varied C programs continually exposed new edge cases and required me to refine the approach. 

Overall, I’d say I really enjoyed the project. The experience showed me that research often involves uncovering new problems as much as solving the original one, and the internship strengthened my interest in pursuing further research. I hope to build on the skills and experience gained during this internship in my bachelor’s thesis and future master’s studies.