# Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation

arXiv: https://arxiv.org/abs/2601.19747 · HTML: https://mlsanity.com/paper/2601.19747/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 20 of its 32 references that are in the map.
- First posted on arXiv 27 Jan 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 20 of 20)

- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [VeriGen: A Large Language Model for Verilog Code Generation](https://mlsanity.com/paper/2308.00708/) (2023)
- [ChipNeMo: Domain-Adapted LLMs for Chip Design](https://mlsanity.com/paper/2311.00176/) (2023)
- [RTLLM: An Open-Source Benchmark for Design RTL Generation with Large Language Model](https://mlsanity.com/paper/2308.05345/) (2023)
- [OpenCoder: The Open Cookbook for Top-Tier Code Large Language Models](https://mlsanity.com/paper/2411.04905/) (2024)
- [ChatEDA: A Large Language Model Powered Autonomous Agent for EDA](https://mlsanity.com/paper/2308.10204/) (2023)
- [RTLFixer: Automatically Fixing RTL Syntax Errors with Large Language Models](https://mlsanity.com/paper/2311.16543/) (2023)
- [BetterV: Controlled Verilog Generation with Discriminative Guidance](https://mlsanity.com/paper/2402.03375/) (2024)
- [VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool](https://mlsanity.com/paper/2408.08927/) (2024)
- [AutoChip: Automating HDL Generation Using LLM Feedback](https://mlsanity.com/paper/2311.04887/) (2023)
- [Revisiting VerilogEval: A Year of Improvements in Large-Language Models for Hardware Code Generation](https://mlsanity.com/paper/2408.11053/) (2024)
- [AutoVCoder: A Systematic Framework for Automated Verilog Code Generation using LLMs](https://mlsanity.com/paper/2407.18333/) (2024)
- [QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation](https://mlsanity.com/paper/2505.24183/) (2025)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [MAGE: A Multi-Agent Engine for Automated RTL Code Generation](https://mlsanity.com/paper/2412.07822/) (2024)
- [DeepRTL: Bridging Verilog Understanding and Generation with a Unified Representation Model](https://mlsanity.com/paper/2502.15832/) (2025)
- [Large Language Model for Verilog Generation with Code-Structure-Guided Reinforcement Learning](https://mlsanity.com/paper/2407.18271/) (2024)
- [QiMeng-SALV: Signal-Aware Learning for Verilog Code Generation](https://mlsanity.com/paper/2510.19296/) (2025)
- [REvolution: An Evolutionary Framework for RTL Generation driven by Large Language Models](https://mlsanity.com/paper/2510.21407/) (2025)

## Built on by (most cited first, 3 of 3)

- [COEVO: Co-Evolutionary Framework for Joint Functional Correctness and PPA Optimization in LLM-Based RTL Generation](https://mlsanity.com/paper/2604.15001/) (2026)
- [AutoSurrogate: An LLM-Driven Multi-Agent Framework for Autonomous Construction of Deep Learning Surrogate Models in Subsurface Flow](https://mlsanity.com/paper/2604.11945/) (2026)
- [SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs](https://mlsanity.com/paper/2608.29841/) (2026)

## Abstract (arXiv)

In the rapidly evolving field of Electronic Design Automation (EDA), the deployment of Large Language Models (LLMs) for Register-Transfer Level (RTL) design has emerged as a promising direction. However, silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations introduced by iterative debugging, and (iii) semantic drift as intent is reinterpreted across agent handoffs. In this work, we propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs. By integrating a multi-branch verification pipeline that combines trace-driven temporal analysis with formal verification consisting of assertion-based checking and boolean equivalence proofs, Veri-Sure enables functional correctness beyond pure simulations. We also introduce VerilogEval-v2-EXT, extending the original benchmark with 53 more industrial-grade design tasks and stratified difficulty levels, and show that Veri-Sure achieves state-of-the-art verified-correct RTL code generation performance, surpassing standalone LLMs and prior agentic systems.