# Saarthi: The First AI Formal Verification Engineer

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 24 references that are in the map.
- First posted on arXiv 23 Feb 2025.

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Sparks of Artificial General Intelligence: Early experiments with GPT-4](https://mlsanity.com/paper/2303.12712/) (2023)
- [AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation](https://mlsanity.com/paper/2308.08155/) (2023)
- [Improving Factuality and Reasoning in Language Models through Multiagent Debate](https://mlsanity.com/paper/2305.14325/) (2023)
- [Gorilla: Large Language Model Connected with Massive APIs](https://mlsanity.com/paper/2305.15334/) (2023)
- [OpenHands: An Open Platform for AI Software Developers as Generalist Agents](https://mlsanity.com/paper/2407.16741/) (2024)
- [ChatDev: Communicative Agents for Software Development](https://mlsanity.com/paper/2307.07924/) (2023)
- [MM-REACT: Prompting ChatGPT for Multimodal Reasoning and Action](https://mlsanity.com/paper/2303.11381/) (2023)
- [More Agents Is All You Need](https://mlsanity.com/paper/2402.05120/) (2024)
- [All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification](https://mlsanity.com/paper/2403.16750/) (2024)
- [Generative AI Augmented Induction-based Formal Verification](https://mlsanity.com/paper/2407.18965/) (2024)

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

- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)
- [FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures](https://mlsanity.com/paper/2510.15906/) (2025)
- [Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification](https://mlsanity.com/paper/2605.06434/) (2026)
- [Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification](https://mlsanity.com/paper/2603.03175/) (2026)
- [Agentic AI-based Coverage Closure for Formal Verification](https://mlsanity.com/paper/2603.03147/) (2026)
- [A Survey on LLM-Integrated Hardware Design Verification](https://mlsanity.com/paper/2610.10580/) (2026)

## Abstract (arXiv)

Recently, Devin has made a significant buzz in the Artificial Intelligence (AI) community as the world's first fully autonomous AI software engineer, capable of independently developing software code. Devin uses the concept of agentic workflow in Generative AI (GenAI), which empowers AI agents to engage in a more dynamic, iterative, and self-reflective process. In this paper, we present a similar fully autonomous AI formal verification engineer, Saarthi, capable of verifying a given RTL design end-to-end using an agentic workflow. With Saarthi, verification engineers can focus on more complex problems, and verification teams can strive for more ambitious goals. The domain-agnostic implementation of Saarthi makes it scalable for use across various domains such as RTL design, UVM-based verification, and others.