💬 NLP

CktFormalizer: Autoformalization of Natural Language into Circuit Representations

CktFormalizer is a framework that leverages Lean 4's dependently-typed HDL to guide LLMs in generating hardware descriptions that are guaranteed to be syntactically correct, free of synthesis-breaking defects, and functionally verified through machine-checked proofs, thereby achieving near-perfect backend realizability and enabling safe, automated PPA optimization.

Original authors: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Published 2026-05-11

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are asking a very talented but slightly careless architect to draw a blueprint for a house based on a verbal description.

In the traditional world of chip design, you would ask the architect to write the instructions in Verilog (a language used to describe computer chips). The architect might write a beautiful description, but because Verilog is a bit like a loose set of rules, the architect might accidentally say, "Connect a 4-inch pipe to an 8-inch pipe," or "Create a hallway that loops back into itself."

The computer checks the grammar and says, "Looks good!" But when the house is actually built (the chip is manufactured), those mistakes cause the pipes to burst or the hallway to trap people. These are expensive, silent failures that only show up weeks later.

CKTFORMALIZER is a new framework that changes the game. Instead of letting the architect write directly in the loose language of Verilog, it forces them to write in a strict, mathematical language called Lean.

Here is how it works, using a simple analogy:

1. The Strict Editor (The Compiler)

Think of Lean as a super-strict editor who knows exactly how a house must be built.

The Old Way: The architect writes "Connect pipe A to pipe B." The editor doesn't check sizes. Later, the construction crew finds out Pipe A is too small.
The CKTFORMALIZER Way: The architect tries to write "Connect Pipe A (size 4) to Pipe B (size 8)." The editor immediately slams the door and says, "Error! You cannot connect these. Fix it now."
The Result: The architect (an AI) gets instant feedback. They can't move forward until the sizes match perfectly. This catches "width mismatches" and "loops" before a single brick is laid.

2. The Safety Net (Type Safety)

In the old system, you might accidentally leave a door open in a room, and the house is built with a drafty, broken room. In the Lean system, the rules are so strict that it is physically impossible to write a blueprint with a broken room.

If the architect forgets to describe what happens when a switch is flipped, the editor says, "You missed a case! You must describe every possibility."
This ensures that the design is "correct by construction." If it compiles (passes the editor's check), it is guaranteed to be structurally sound.

3. The Proof of Truth (Formal Verification)

Usually, to check if a house design works, you build a tiny model and test it. Sometimes the model works, but the real house doesn't.
CKTFORMALIZER uses mathematical proofs. The AI doesn't just guess; it writes a mathematical proof that says, "This new, cheaper design does exactly the same thing as the original perfect design."

It's like having a mathematician prove that your new, cheaper blueprint is 100% identical in function to the original, down to the last atom, for every possible scenario, not just the ones you tested.

4. The Optimization Loop (The Smart Renovator)

Once the AI has a design that works, the system doesn't stop. It acts like a smart renovator who looks at the blueprint and says, "We can make this house 35% smaller and use 30% less energy."

The AI tries to rearrange the rooms (the circuit logic).
It builds a new version.
It immediately runs the "Strict Editor" again to make sure the new version still works perfectly.
It then runs a physical simulation to see how much space and power it saves.
If the new version is better and still mathematically proven to be correct, it keeps it. If not, it rolls back.

The Results

The paper tested this on hundreds of design problems (like building counters, memory units, and traffic light controllers).

The Baseline (Old Way): When they tried to build the chips, about 20% of the designs that looked correct on paper actually failed when they tried to manufacture them.
CKTFORMALIZER (New Way): 100% of the designs that passed the strict editor successfully made it through the entire manufacturing process (synthesis, placement, and routing) without failing.
Efficiency: The system also managed to shrink the designs and save power significantly (up to 35% less area) while proving they were still perfect.

In Summary

CKTFORMALIZER is like giving an AI architect a magic rulebook that prevents them from making mistakes before they even start drawing. Instead of building a house and hoping it doesn't collapse, it forces the architect to prove the house is solid before the first brick is ordered. This turns chip design from a game of "guess and check" into a process of "prove and build," resulting in chips that are smaller, more efficient, and guaranteed to work.

Technical Summary: CktFormalizer

Problem Statement

Hardware design remains an error-prone discipline where subtle defects, such as bit-width mismatches, combinational loops, or incomplete case logic in Finite State Machines (FSMs), can pass syntax checks but fail silently during synthesis or manifest as costly silicon bugs later. While Large Language Models (LLMs) have demonstrated the ability to generate Verilog from natural language specifications, the resulting code often inherits the inherent pitfalls of Verilog and VHDL: a lack of static guarantees like dependent types, exhaustive pattern matching, and machine-checked proofs. Consequently, LLM-generated hardware frequently requires extensive manual debugging and often fails to reach physical implementation (Place-and-Route, DRC, LVS) even when functionally correct in simulation.

Methodology

The paper presents CktFormalizer, a framework that unifies LLM-driven code generation with formal verification by targeting a dependently-typed Hardware Description Language (HDL) embedded in Lean 4. Rather than generating Verilog directly, the system redirects the LLM agent to generate Lean code, which serves as the primary compilation target.

Core Architecture

The framework operates through a closed-loop pipeline involving three distinct roles for Lean:

Type Checker (Compile-Time Verifier): Lean's dependent type system encodes bit-width constraints, case coverage, and acyclicity. Hardware defects (e.g., width mismatches or combinational loops) are caught as compile-time type errors rather than silent backend failures. This provides the LLM agent with immediate, actionable feedback to iteratively repair the design.
Correctness Firewall: Designs that successfully compile in Lean are structurally guaranteed to be free of specific classes of defects (width mismatches, combinational loops, unintended latches). This ensures that compiled designs survive the backend synthesis and Place-and-Route (P&R) flow without the 20% loss rate observed in baseline Verilog generation.
Proof Assistant: The agent constructs automated theorem proofs to verify functional equivalence between the natural language specification and the generated (or optimized) implementation. These proofs cover arbitrary input sequences and parameterized widths, going beyond the limitations of bounded SMT-based checking.

Workflow

Generation & Iteration: An LLM agent (instantiated with Claude) generates Lean HDL code based on a natural language specification. It enters an iterative "generate-compile-repair" loop where Lean compiler errors guide the agent to fix semantic bugs before they propagate.
Extraction: Upon successful compilation, a metaprogram (#synthesizeVerilog) extracts synthesizable SystemVerilog from the Lean Signal combinator graph.
Physical Implementation: The extracted SystemVerilog is simulated, synthesized (using Yosys), and physically implemented (using OpenROAD with the SkyWater 130nm PDK) to generate GDSII layouts and Power-Performance-Area (PPA) metrics.
PPA Optimization Loop: A closed-loop optimization stage feeds PPA metrics back to the agent. The agent proposes architectural variants (e.g., parallel vs. serial datapaths) and must provide machine-checked equivalence proofs to ensure the optimized variant remains functionally equivalent to the original specification.

Key Contributions

First End-to-End Framework: CktFormalizer is the first framework to combine LLM-driven hardware generation with a Lean-embedded HDL, providing a pipeline from natural language to synthesizable silicon with closed-loop PPA optimization.
Type-Guided Generation: The paper demonstrates that targeting a type-safe HDL substantially improves LLM success rates compared to direct Verilog generation. Compile-time type errors provide structured feedback that guides the agent toward correct designs, scaling to industry-relevant IP like multi-channel handshake bus interfaces.
Formal Verification Integration: The framework bridges the gap between LLM-generated code and provably correct hardware by enabling the agent to produce machine-checked equivalence proofs. This ensures that architectural optimizations do not compromise functional correctness.

Experimental Results

The framework was evaluated on three benchmarks: VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems).

Backend Realizability: A critical finding is that CktFormalizer preserves functional correctness through the backend. While the baseline (direct Verilog generation) loses approximately 20% of functionally correct designs during synthesis and routing, CktFormalizer preserves 100% of its compiled designs through the full synthesis, P&R, DRC, and LVS flow.
Compilation and Simulation: On VerilogEval, CktFormalizer achieved a 92.3% Lean compilation rate and a 72.4% RTL simulation pass rate, competitive with direct Verilog generation baselines. When synthesis feedback is included in the agent loop, the compilation rate rises to 99.4%.
PPA Optimization: The closed-loop optimization stage yielded significant improvements. Through validated architecture exploration, the framework achieved up to 35% area reduction and 30% power reduction.
Timing Closure: All functionally correct designs that completed Place-and-Route achieved timing closure (WNS $\ge$ 0 ns) without manual intervention.
Proof Generation: In a pilot study, stepwise proof generation (iterative refinement with proof-goal feedback) improved proof completion rates from 53% to 63%, demonstrating the viability of proof assistants for hardware verification.

Significance and Claims

The paper claims that dependent types and LLM agents are complementary. By using a formal language (Lean) as both the generation target and the verification substrate, the framework transforms the LLM's "generate-and-test" loop from a stochastic search over syntactically valid programs into a type-guided refinement process.

The authors emphasize that the compiler acts as the verifier, shifting error detection from the end of the EDA pipeline (where fixes are costly) to compile time. This approach allows the system to produce hardware that is not only functionally correct but also structurally robust against backend transformations, effectively solving the "silent failure" problem common in LLM-generated hardware. The work suggests that formal languages can serve as a foundation for trustworthy, automated hardware design, enabling LLMs to navigate the complex trade-offs of hardware optimization while maintaining rigorous correctness guarantees.