CktFormalizer: Autoformalization of Natural Language into Circuit Representations

The gist: CKTFORMALIZER is a framework that redirects LLM-driven hardware generation through a dependently-typed HDL embedded in Lean, which serves as a type checker, correctness firewall, and proof assistant to ensure high backend realizability for hardware designs<ref:2605.07782#pg14>

How it works

CKTFORMALIZER unifies LLM-driven code generation with formal verification by targeting a dependently-typed hardware domain-specific language (DSL) embedded in Lean<ref:2605.07782#pg5> Given a natural language specification, an LLM agent generates hardware whose bit-width safety, loop freedom, and case exhaustiveness are enforced at compile time<ref:2605.07782#pg4> The key insight is that the compiler is the verifier rather than generating Verilog and hoping it is correct<ref:2605.07782#pg2> This transforms the LLM’s generate-and-test loop from a stochastic search over syntactically valid programs into a type-guided refinement process that systematically narrows the space of candidate designs<ref:2605.07782#pg4>

Type Safety and Structural Guarantees

Lean’s dependent type system encodes bit widths at the type level via BitVec N, turning width mismatches into compile-time errors rather than silent bugs<ref:2605.07782#pg2> Combinational logic forms a DAG enforced by the Signal monad; state feedback requires explicit register primitives (Signal.register, Signal.loop), making combinational loops impossible by construction Furthermore, Lean’s exhaustive pattern matching prevents unintended latches For sequential circuits, CKTFORMALIZER provides an imperative Signal.circuit macro that desugars into Signal.loop and Signal.register calls, enabling natural descriptions of pipelines and state machines

The End-to-End Pipeline

The framework follows a closed-loop PPA optimization stage where the agent receives immediate, actionable feedback from Lean’s type system at every iteration<ref:2605.07782#pg2> The automated evaluation pipeline assesses designs through a sequence of increasingly stringent checks, including type correctness and Verilog extraction A successful build confirms that the design is semantically well-formed and produces a synthesizable.sv file Designs that pass RTL simulation are sent to the physical-design flow, where Yosys synthesizes each design to the SkyWater 130nm HD standard-cell library through the OpenROAD Flow Docker environment

Formal Verification and Optimization

A unique capability of Lean HDL is that hardware designs can be formally verified within the same language used to describe them, because signals have a denotational semantics as functions over time (Signal dom α ≜ N → α) The agent can also produce machine-checked equivalence proofs between specifications and optimized implementations, bridging the gap between agentic code generation and machine-checked verification For PPA optimization, the agent uses 'lean proof step' to state 'theorem equiv: = spec:= by sorry' and then replaces 'sorry' with tactics until no goals remain

Experimental Results

CKTFORMALIZER achieves simulation pass rates competitive with direct Verilog generation while delivering substantially higher backend realizability, where 95–100% of compiled designs complete the full synthesis, place-and-route, DRC, and LVS flow A closedloop PPA optimization stage yields up to 35% area reduction and 30% power reduction through validated architecture exploration Architecture exploration can yield up to 35% area reduction when an LLM agent receives concrete synthesis metrics, demonstrating the ability to reason about hardware trade-offs at the architectural level The framework shows that designs generated by CIRCFORMALIZER are free of width mismatches, combinational loops, and incomplete case analysis by construction

Conclusion

The results show that dependent types and LLM agents are complementary—formal languages serve as both generation targets and verification substrates for trustworthy hardware design This approach provides structured feedback that guides the agent toward correct designs, transforming the LLM’s loop into a type-guided refinement process The framework successfully produces formally verified hardware, including machine-checked equivalence proofs between specifications and optimized implementations The paper concludes that CKTFORMALIZER provides an end-to-end pipeline from natural language to synthesizable silicon with closed-loop PPA optimization

How it works

CKTFORMALIZER is a framework that redirects LLM-driven hardware generation through a dependently-typed HDL embedded in Lean<ref:2605.07782#pg5> Lean serves three roles: (i) type checker:dependent types encode bit-width constraints, case coverage, and acyclicity, turning hardware defects into compile-time errors that guide iterative repair; (ii) correctness firewall:compiled designs are structurally free of defects that cause silent backend failures (the baseline loses 20% of correct designs during synthesis and routing; CKTFORMALIZER preserves all of them); (iii) proof assistant:the agent constructs automated theorem equivalence proofs over arbitrary input sequences and parameterized widths, beyond the reach of bounded SMT-based checking<ref:2605.07782#pg4>

Type Safety and Structural Guarantees

Lean’s dependent type system encodes bit widths at the type level via BitVec N, turning width mismatches into compile-time errors rather than silent bugs<ref:2605.07782#pg2> Combinational logic forms a DAG enforced by the Signal monad; state feedback requires explicit register primitives (Signal.register, Signal.loop), making combinational loops impossible by construction Lean’s exhaustive pattern matching further prevents unintended latches

The End-to-End Pipeline

The framework follows a closed-loop PPA optimization stage where the agent receives immediate, actionable feedback from Lean’s type system at every iteration<ref:2605.07782#pg2> The automated evaluation pipeline assesses designs through a sequence of increasingly stringent checks, including type correctness and Verilog extraction A successful build confirms that the design is semantically well-formed and produces a synthesizable.

1. Direct generation of hardware descriptions from natural language specifications is improved by redirecting LLM-driven generation through a dependently-typed HDL embedded in Lean 4, ensuring bit-width safety, loop freedom, and case exhaustiveness are enforced at compile time.

2. The improved system can perform automated theorem equivalence proofs between specifications and optimized implementations, as the framework allows the agent to construct automated theorem equivalence proofs over arbitrary input sequences and parameterized widths, beyond the reach of bounded SMT-based checking.

3. Hardware optimization is transformed from a manual, expert-driven process into an automated, iterative refinement loop where a closed-loop PPA optimization stage feeds synthesis metrics back to the agent for iterative refinement with equivalence guarantees, yielding up to 35% area reduction and 30% power reduction.

4. The system can discover superior architectures by leveraging synthesis feedback, as the LLM agent can reason about hardware trade-offs at the architectural level, leading to discovering structurally distinct implementations rather than merely tuning parameters.

5. A fully automated pipeline is established that ensures backend readiness: "98.6% of compiled designs produce physical layouts through the full synthesis and P&R flow, guaranteeing that designs are free of width mismatches, combinational loops, and incomplete case analysis by construction."

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/