# Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 29 references that are in the map.
- First posted on arXiv 3 Mar 2026.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Sparks of Artificial General Intelligence: Early experiments with GPT-4](https://mlsanity.com/paper/2303.12712/) (2023)
- [Billion-scale similarity search with GPUs](https://mlsanity.com/paper/1702.08734/) (2017)
- [From Local to Global: A Graph RAG Approach to Query-Focused Summarization](https://mlsanity.com/paper/2404.16130/) (2024)
- [Leveraging Passage Retrieval with Generative Models for Open Domain Question Answering](https://mlsanity.com/paper/2007.01282/) (2020)
- [Knowledge Graphs](https://mlsanity.com/paper/2003.02320/) (2020)
- [Precise Zero-Shot Dense Retrieval without Relevance Labels](https://mlsanity.com/paper/2212.10496/) (2022)
- [Comprehensive Verilog Design Problems: A Next-Generation Benchmark Dataset for Evaluating Large Language Models and Agents on RTL Design and Verification](https://mlsanity.com/paper/2506.14074/) (2025)
- [All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification](https://mlsanity.com/paper/2403.16750/) (2024)
- [Revolution or Hype? Seeking the Limits of Large Models in Hardware Design](https://mlsanity.com/paper/2509.04905/) (2025)
- [Saarthi: The First AI Formal Verification Engineer](https://mlsanity.com/paper/2502.16662/) (2025)
- [BugGen: A Self-Correcting Multi-Agent LLM Pipeline for Realistic RTL Bug Synthesis](https://mlsanity.com/paper/2506.10501/) (2025)
- [Hey AI, Generate Me a Hardware Code! Agentic AI-based Hardware Design & Verification](https://mlsanity.com/paper/2507.02660/) (2025)
- [Generative AI Augmented Induction-based Formal Verification](https://mlsanity.com/paper/2407.18965/) (2024)

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

- [Exploring the Agentic Frontier of Verilog Code Generation](https://mlsanity.com/paper/2603.19347/) (2026)

## Abstract (arXiv)

Saarthi is an agentic AI framework that uses multi-agent collaboration to perform end-to-end formal verification. Even though the framework provides a complete flow from specification to coverage closure, with around 40% efficacy, there are several challenges that need to be addressed to make it more robust and reliable. Artificial General Intelligence (AGI) is still a distant goal, and current Large Language Model (LLM)-based agents are prone to hallucinations and making mistakes, especially when dealing with complex tasks such as formal verification. However, with the right enhancements and improvements, we believe that Saarthi can be a significant step towards achieving domain-specific general intelligence for formal verification. Especially for problems that require Short Term, Short Context (STSC) capabilities, such as formal verification, Saarthi can be a powerful tool to assist verification engineers in their work. In this paper, we present two key enhancements to the Saarthi framework: (1) a structured rulebook and specification grammar to improve the accuracy and controllability of SystemVerilog Assertion (SVA) generation, and (2) integration of advanced Retrieval Augmented Generation (RAG) techniques, such as GraphRAG, to provide agents with access to technical knowledge and best practices for iterative refinement and improvement of outputs. We also benchmark these enhancements for the overall Saarthi framework using challenging test cases from NVIDIA's CVDP benchmark targeting formal verification. Our benchmark results stand out with a 70% improvement in the accuracy of generated assertions, and a 50% reduction in the number of iterations required to achieve coverage closure.