One typed loop. Compiler diagnostics, proof states, simulation, and PPA feedback all become actionable signals for the hardware agent.
91.1–99.4%compile pass across four benchmarks
95.4–100%physical-design pass among RTL-sim-passing designs
+10 ppkernel-accepted proof completion with stepwise feedback
−58.6%maximum synthesis-area reduction in the PPA loop
01 · The foundation
A circuit IR that makes mistakes visible early.
CktLean extends Sparkle’s typed hardware representation, elaboration, and backend lowering. Widths, state, signedness, and clock domains remain explicit as a design moves from Lean source to SystemVerilog.
The persistent Lean REPL turns compiler diagnostics and proof goals into feedback an agent can use. That gives CktFormalizer a structured loop for generation, repair, optimization, and source-level equivalence proving.
Parameterized state and memory
Dynamic bit operations and signed arithmetic
Multiple clock domains
Exhaustive case handling
Kernel-checked source equivalence
CapabilitySystemVerilogCktLean
Width consistency✕✓
Register-guarded feedback✕✓
Total case handling✕✓
Primary diagnosticsTool logsType / macro errors
Kernel-checked proofs✕✓
Auto SystemVerilog extractionN/A✓
Supported generation subset · summarized from Table 1 in the paper.
Typed hardware representation. An 8-bit counter uses explicit register feedback, while adding incompatible widths is rejected by Lean’s type checker.
02 · The agentic loop
From intent to physically realizable hardware.
CktFormalizer separates three kinds of correctness and lets each tool report back at the stage where it has the most leverage.
Figure 2. The agent receives a natural-language specification and examples, then iterates through Lean compilation, proof development, RTL simulation, synthesis, place-and-route, and PPA feedback.
STEP 01SpecifyNatural-language intent, benchmark examples, and a Lean exemplar.
STEP 02Generate + repairLean HDL is compiled in a persistent REPL; diagnostics guide edits.
STEP 03VerifyProve source-level properties, then evaluate emitted RTL.
STEP 04OptimizeUse synthesis and P&R metrics to explore and refine architectures.
⌁/ 01
Structural
Lean checks bit widths, ports, clock-domain parameters, and exhaustive pattern matches before RTL extraction.
∴/ 02
Formal
Kernel-accepted lemmas establish circuit-to-specification or implementation-to-implementation equivalence under explicit assumptions.
◉/ 03
Functional
Reference simulation and RTL equivalence checks test whether the generated design behaves as intended on exercised traces.
03 · Evidence
High compile coverage, then the hard part: backend reality.
Select a benchmark to inspect the end-to-end pass rates reported in Table 3. Values are percentages; downstream columns are conditioned on RTL simulation passing.
VerilogEval · 156 problems
04 · Proof + PPA
Feedback does more than fix errors. It changes what the agent can search.
Stepwise proof states improve formal completion, while synthesis feedback enables architecture exploration and correctness-aware PPA optimization.
Interactive proof replay · verified trace
A real 8-bit edge detector, opened one goal at a time.
This is the circuit from Benchmark/Prob054_edgedetect.lean. Pick an input trace to run the sequential logic, then advance the same four tactics accepted by the local Lean REPL.
PROB054BitVec 84 tactics
01
Run the circuit
TRACE READY
At cycle t, d_last remembers in[t−1]; pedge registers the detected edge.
ind_lastin & ~d_lastpedge
02
Replay the proof
GOAL 1 / 5
CktLean REPL · goal state1 goal
✓
Kernel-accepted source trace. The replay mirrors the checked sequence unfold → dsimp only → change → rfl. It is a deterministic presentation of that verified trace; the page does not pretend to run Lean in the browser.
Run the trace on the left to see the sequential behavior, then advance one tactic at a time. On a 30-problem VerilogEval pilot, stepwise refinement raised kernel-accepted proof completion from 53.3% to 63.3%.
63.3%kernel-accepted proofs with stepwise feedback
Compile pass77% → 100%
Simulation50% → 70%
Yosys equivalence70% → 73%
Optimization and verification signals. The paper reports non-monotonic but accepted design trajectories, area and power reductions, proof-generation gains, and post-route timing closure.
FSM (Lemmings)
35.2% area
9-to-1 multiplexer
27.3% area
Add/Sub unit
17.4% area
Maximum loop reduction
58.6% area
The acceptance rule keeps a candidate only when it passes evaluation, improves at least one metric beyond the threshold, and avoids unacceptable regressions in the other metrics.
Lean REPLcompile + proof state
Icarus Veriloglint + simulation
Yosyssynthesis + formal
OpenROADP&R + timing
KLayoutphysical signoff
SkyWater 130 nmstandard-cell PDK
05 · Reference
Cite CktFormalizer
The paper is available on arXiv, and the code is on GitHub.
@article{cktformalizer2026,
title = {CktFormalizer: Autoformalization of Natural Language into Circuit Representations},
author = {Jing Xiong and Qi Han and Chenchen Ding and He Xiao and Chaofan Tao and Zunhai Su and Qingyao Yang and Xiachong Feng and Kailai Yang and Ngai Wong},
journal = {arXiv preprint arXiv:2605.07782},
year = {2026},
url = {https://arxiv.org/abs/2605.07782}
}
