Research Seminar by Dr Subhajit Roy | Bridging Logic and Language: Program Verification in the LLM Era

Bridging Logic and Language: Program Verification in the LLM Era

Program verification has stood as one of the enduring challenges in computer science. Despite decades of progress, many verification problems remain beyond the reach of even the most advanced verification engines. A central difficulty lies in the need for human insight—the ability to identify the right invariants, ranking functions, or proof strategies that make verification succeed. While numerous heuristics have been developed to approximate this reasoning, the gap has persisted. In our work, we ask a simple but powerful question: Can Large Language Models provide these missing insights? We explore how the creative reasoning capabilities of LLMs can be combined with the precision and rigor of formal methods—developed and refined over the past half-century—to advance the automation frontier in verification. This talk will present our recent efforts in using LLMs to infer proof artifacts such as inductive invariants for correctness and ranking functions for termination, to refactor code for migration into memory-safe dialects of C, and to learn idiomatic templates for what we call “angelic verification.” We believe that the convergence of LLMs and formal verification represents a promising new direction—one that could transform how we approach the problem of proving programs correct.