# CktFormalizer: Autoformalization of Natural Language into Circuit Representations

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 17 of its 43 references that are in the map.
- First posted on arXiv 8 May 2026.

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [VerilogEval: Evaluating Large Language Models for Verilog Code Generation](https://mlsanity.com/paper/2309.07544/) (2023)
- [VeriGen: A Large Language Model for Verilog Code Generation](https://mlsanity.com/paper/2308.00708/) (2023)
- [RTLLM: An Open-Source Benchmark for Design RTL Generation with Large Language Model](https://mlsanity.com/paper/2308.05345/) (2023)
- [Chip-Chat: Challenges and Opportunities in Conversational Hardware Design](https://mlsanity.com/paper/2305.13243/) (2023)
- [Benchmarking Large Language Models for Automated Verilog RTL Code Generation](https://mlsanity.com/paper/2212.11140/) (2022)
- [ChipGPT: How far are we from natural language hardware design](https://mlsanity.com/paper/2305.14019/) (2023)
- [DAVE: Deriving Automatically Verilog from English](https://mlsanity.com/paper/2009.01026/) (2020)
- [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)
- [CodeV: Empowering LLMs with HDL Generation through Multi-Level Summarization](https://mlsanity.com/paper/2407.10424/) (2024)

## Abstract (arXiv)

Hardware infrastructure is a critical bottleneck for LLM-driven circuit design, limiting what agents can express, compile, and iteratively refine within an agentic loop. To address this bottleneck, we introduce CKTLEAN, a typed hardware infrastructure embedded in Lean. It supports hardware description, compilation to SystemVerilog, and interactive type-checking and proof feedback through a persistent read-eval-print loop (REPL). On this foundation, we build CKTFORMALIZER, an agent framework for hardware generation, repair, optimization, and source-level equivalence proving. We evaluate structural correctness through compilation, functional correctness through RTL and gate-level simulation, and formal correctness through proofs relative to stated specifications. Across VerilogEval, RTLLM, ResBench, and CVDP, CKTFORMALIZER with CKTLEAN achieves compilation rates of 91.1%-99.4%. Among designs that pass RTL simulation, 95.4%-100.0% jointly complete synthesis and place-and-route and pass design-rule and layout-versus-schematic checks. In a separate evaluation on 30 VerilogEval problems, interactive proof-state feedback raises kernel-accepted equivalence proof completion from 53.3% to 63.3%. Hardware evaluation feedback also guides architecture exploration and iterative power, performance, and area (PPA) optimization, with synthesis-area reductions of up to 58.6% in the optimization loop. These results suggest that typed representations and explicit proof-state feedback help structure the agentic loop: compiler diagnostics guide targeted repairs, while proof-state feedback helps agents identify what remains to be proved and determine the next proof step. Project Page: https://ckt-formalizer.github.io/