Evaluating AI-Generated Formal Verification Harnesses for RTL Using an Open-Source, Non-Vacuity-Aware Flow

We present an open-source, reproducible workflow to evaluate AI-generated formal verification harnesses for RTL, focusing on proof soundness rather than property generation alone. In contrast to prior AI-assisted formal approaches centred on proprietary tools or agent orchestration, our method targets harness quality in a Yosys-based flow. We implement automated non-vacuity checks using cover-reachability tests and assumption-ablation runs to expose over-constrained environments and misleading proofs. Evaluated across multiple RTL design classes and SMT solvers, the framework enables controlled, tool-agnostic benchmarking and provides practical guidance on when AI-generated assumptions and assertions yield trustworthy formal results.

Ramesh Krishnamurthy is a Postdoctoral Research Associate at the University of Edinburgh working on AI-assisted formal verification and verification automation for electronic systems. His work combines formal methods, verification, and machine learning, with recent focus on AI-supported RTL formal verification flows. He earned his PhD in Computer Science from the University of Antwerp, where his research focused on formal analysis and performance certification of model-predictive control and learning-enabled systems. Prior to academia, he worked in avionics verification and validation under safety-critical certification standards.