formal.org

AI for hardware formal verification: what the research showsTwenty-six research papers on applying AI to hardware design formal verification, selected and summarised for learners. Each entry gives what the authors did, the main result, the key idea for a learner, and the study's limitations. Grouped by what you want to learn to do: writing properties, judging property quality, finding proofs and invariants, debugging counterexamples, and checking AI-generated RTL.Papers

LLM-Assisted Circuit Verification: A Comprehensive Survey — Liu, Lu, Wang, Yao, Yu, ASP-DAC 2026 — Reviews how language models are used across hardware verification, following the steps of a real verification workflow.

LLM Assisted Verification Assertion Generation: Challenges and Future Directions — Mali, Karfa, arXiv 2026 — Reviews methods for generating SystemVerilog assertions with language models and organizes the open challenges, each with key takeaways.

FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware — Kang, Liu, Bany Hamad, Suhaib, Ren, DATE 2025 — The first broad benchmark for language models on formal verification tasks, from translating English into SVA to writing assertions straight from a design. It scores answers by formal equivalence, not text similarity.

AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation — Pulavarthi, Nandal, Dan, Pal, NAACL Findings 2025 — Gives language models 100 open-source Verilog designs, with one or five example designs and their proven assertions, and checks every generated assertion formally.

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models — Cosler, Hahn, Mendoza, Schmitt, Trippel, CAV 2023 — Uses a language model to translate plain-English requirements into temporal logic, and lets the user inspect and correct how each part of the sentence was translated. Not hardware-specific.

Using LLMs to Facilitate Formal Verification of RTL — Orenes-Vera, Martonosi, Wentzlaff, arXiv 2023 — GPT-4 writes assertions for real open-source RTL through the AutoSVA testbench generator.

(Security) Assertions by Large Language Models — Kande, Pearce, Tan, Dolan-Gavitt, Thakur, Karri, Rajendran, IEEE TIFS 2024 — Can a language model write security assertions, such as 'a locked register cannot be written'? Measures how much prompt detail it needs, on designs with known hardware weaknesses.

Spec2Assertion: Automatic Pre-RTL Assertion Generation using Large Language Models with Progressive Regularization — Wu, Pan, Kande, Quinn, Tyagi, Houngninou, Rajendran, Hu, arXiv 2025 — Writes assertions from the specification before any RTL exists, moving in stages from messy English to a semi-formal description to SVA.

FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols — Shih, Lin, Gupta, Malik, arXiv 2025 — For bus protocol specs, candidate assertions come from templates, a formal check keeps only those consistent with the spec's timing diagrams, and the language model only picks among the survivors.

Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification — Krishnamurthy, Chitnis, Prodromakis, arXiv 2026 — Built on Yosys and SymbiYosys. It rejects assertions that pass vacuously or miss injected bugs, picks an SMT solver from the design's structure, and has a language model explain each counterexample in plain English.

AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL — Bai, Bany Hamad, Suhaib, Ren, ICLAD 2025 — Links spec concepts to RTL signals in a knowledge graph so the model writes assertions grounded in both.

SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation — Imperial, Zheng, arXiv 2026 — Translates each generated assertion back into English and has a language model judge whether the spec supports it, contradicts it, or never mentions it.

Large Lemma Miners: Can LLMs Do Induction Proofs for Hardware? — Peled, Kroening, Tautschnig, Vizel, IJCAI 2026 — Language models propose helper lemmas, a checker keeps only those that hold, then finds a set that makes the target property provable by induction.

Neural Model Checking — Giacobbe, Kroening, Pal, Tautschnig, NeurIPS 2024 — Trains a small neural network to act as a proof that something good eventually happens, then an SMT check confirms the proof is valid.

Let a Neural Network Be Your Invariant — Giacobbe, Kroening, Pal, Tautschnig, NeurIPS 2025 — Extends neural proof certificates to cover safety and liveness together, still validated by a solver.

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking — Su, Bu, Yang, Ci, Tian, arXiv 2026 — When induction fails, it shows the language model the offending state and asks for an invariant that rules it out.

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking — Zhou, Hu, Zhang, Zhang, arXiv 2026 — Lightweight online learning picks which generalization strategy the IC3 engine uses, without any language model.

Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking — Fan et al., arXiv 2026 — A language model agent reads the RTL and the IC3 engine's proof state and proposes word-level lemmas. The engine checks every one before accepting it.

LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking — Miao, Hu, Zhang, Zhang, arXiv 2026 — A model pre-trained once predicts useful lemmas for IC3-style engines, with no training per design.

IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking — Miao, Hu, Yang, Zhang, IJCAI 2026 — A language model proposes code changes to an IC3 engine offline. A change is kept only if every result comes with a checkable proof or counterexample.

FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures — Bai, Bany Hamad, Ho, Suhaib, Ren, DVCon U.S. 2026 — Turns a failing trace into a cause-and-effect graph, has a language model argue for and against each suspicious signal, then writes a causal story and proposes an RTL fix.

Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair — Tran, arXiv 2026 — Language model agents write properties, SymbiYosys checks the design, and counterexamples go back to the agents to repair the RTL until k-induction proves it.

All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification — Gadde, Kumar, Nalapat, Rezunov, Cappellini, DVCon U.S. 2024 — Generates tens of thousands of SystemVerilog designs with four language models and uses formal verification to check them for known hardware weaknesses.

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus — Alvanaki, Wang, Seyoum, Carloni, MLCAD 2026 — Generates RTL from several independent model families and uses sequential equivalence checking to find designs that provably agree. Agreement across families becomes a confidence signal, with no testbench needed.

Saarthi: The First AI Formal Verification Engineer — Kumar, Gadde, Kopparam Radhakrishna, Lettnin, DVCon U.S. 2025 — A team of language model agents runs the whole formal flow: verification plan, assertions, proofs, counterexample analysis, and coverage, with a human stepping in when the agents get stuck.

LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs — Müller, Liu, Drechsler, arXiv 2026 — Uses structured, Gherkin-style scenarios as a middle ground between ambiguous English and formal specs, driving both RTL generation and assertions for formal proof.

Levels assume introductory assertion-based verification, bounded model checking and k-induction. Maintained by David Kebo Houngninou — Associate Professor, Computer Science and Engineering, Texas A&M University.