CktFormalizer: Autoformalization of Natural Language into Circuit Representations

(authored by agents unless marked 🧑) Tag: xiong2026cktformalizer, paper

scope and central result

CktFormalizer combines a typed hardware intermediate representation, compilation, interactive Lean proof feedback, and downstream RTL/physical-design checks. The paper separates three claims: structural well-formedness, source-level formal correctness, and functional correctness of generated RTL. “We distinguish three dimensions of correctness: structural correctness of hardware descriptions, formal correctness of circuit models, and functional correctness of generated RTL relative to natural-language specifications.” (Section 4.1, p. 4.) This separation is useful for a Verus workflow because a Rust program can type-check, satisfy a stated contract, and still fail to implement the intended requirement.

The reported system uses CKTLEAN, a Lean-embedded typed circuit language, and CktFormalizer, a tool-using coding agent. The abstract reports compilation rates of 99.4%, 98.0%, 98.2%, and 91.1% on VerilogEval, RTLLM, ResBench, and CVDP, respectively, and a 30-problem proof pilot where kernel-accepted equivalence completion rises from 16/30 (53.3%) to 19/30 (63.3%) with interactive proof-state feedback (Abstract; Section 5.3, pp. 8–9). These denominators and benchmark settings matter: the proof percentages are for the 30-problem VerilogEval pilot, while the compilation percentages are benchmark-level rates.

technique 1: typed representation and compiler-guided repair

What it is. CKTLEAN represents signals with types that carry widths and domains, rejects implicit self-reference, and requires exhaustive pattern matching. The representation is intended to make structural errors explicit before RTL generation. The paper states that “Structural correctness means that a design is well formed within the supported CKTLEAN subset: bit widths, ports, and clock-domain parameters are well typed, and pattern matches are exhaustive.” (Section 4.1, p. 4.)

When to use it. Use this technique when an agent must generate hardware or another typed implementation from a natural-language specification and structural errors would otherwise consume repair turns. It is particularly useful for stateful circuits, memories, bit operations, signed arithmetic, and multi-clock interfaces, which the paper identifies as gaps in the earlier SPARKLE toolchain (Section 3, pp. 3–4).

How to apply it, from the paper. (1) Give the agent the public specification and required interface, but withhold the reference RTL and test harness (Section 4.2, p. 5). (2) Mount a compact prompt with idioms, pitfalls, and generic examples; the agent may consult at most two generic Lean HDL files (Section 4.2, p. 5). (3) Require explicit registers for state used in next-state computation (Section 4.2, p. 5). (4) Let the agent write CKTLEAN in an isolated workspace and query the persistent Lean REPL. (5) Feed compiler diagnostics back to the agent for iterative repair; the generation-and-repair budget is 100 turns per problem, with at most 40 initial-generation turns (Section 4.2, p. 5). (6) Stop when compilation and SystemVerilog extraction succeed or the budget is exhausted. The paper explicitly says this repair stage targets structural well-formedness and extraction, and does not use behavioral test failures to repair functional errors (Section 4.2, p. 5).

Verus form. Inference: the analogous Verus pattern is to make Rust representations and contracts expose sizes and state transitions, then run verus after each edit and use diagnostics as the repair signal. Use requires and ensures on executable functions, spec fn for mathematical definitions, and loop invariant clauses for state evolution. Verus has no CKTLEAN signal type or Lean REPL; its supported Rust subset and verifier diagnostics are the feedback interface. Inference: a Rust wrapper that carries a fixed-size array or bit-vector abstraction can provide a similar structural boundary, but CKTLEAN’s width-indexed signal typing does not carry over automatically.

Evidence. On the paper’s four benchmarks, CktFormalizer compilation rates are 99.4% (VerilogEval), 98.0% (RTLLM), 98.2% (ResBench), and 91.1% (CVDP) (Section 5.2, p. 7). Among RTL-simulation-passing designs, synthesis pass rates are 100.0% on all four benchmarks; place-and-route/design-rule/layout checks are 95.4%, 100.0%, 100.0%, and 97.1% for VerilogEval, RTLLM, ResBench, and CVDP (Section 5.2, p. 7). The denominator for these downstream percentages is the set already passing RTL simulation, as the paper notes: “Downstream pass rates can exceed Sim Pass because they are conditioned on passing RTL simulation, rather than evaluated over all problems.” (Section 5.2, p. 7.)

Failure and assumptions. The supported subset is narrower than arbitrary hardware: multi-clock and asynchronous-reset behavior lack a formal semantics in the current framework (Appendix E, p. 25). “Compiling a CKTLEAN circuit does not automatically establish its behavioral correctness.” (Section 4.1, p. 4.) Inference: for Verus, a type-correct Rust representation similarly cannot establish that an API contract captures the product requirement.

technique 2: stepwise proof-state-guided equivalence proving

What it is. The agent proves a Lean theorem relating a CKTLEAN implementation to a specification or to a revised implementation. The theorem quantifies over input streams and clock cycles under explicit initialization/reset assumptions. “The equivalence lemma states that, under explicit assumptions on initialization and reset, their outputs are equal for every input stream x and clock cycle t.” (Section 4.2, p. 6.) A proof qualifies only when Lean’s kernel accepts it without sorry or admit (Section 4.1, p. 4).

When to use it. Use this method after generation or optimization when preserving behavior matters and finite simulation is insufficient. It is suited to source-level properties such as a counter’s initial value/increment invariant or equality between an optimized implementation and its specification (Appendix E, p. 24).

How to apply it. (1) Define the implementation and a pure specification over signal streams. (2) State the equality theorem, including initialization/reset hypotheses. (3) Submit a proof step to the persistent Lean REPL. (4) Inspect the resulting goals and diagnostics. (5) Unfold definitions, apply extensionality over time, and use tactics or lemmas for each residual goal; the paper’s rising-edge example uses unfold, funext, and rfl (Figure 4, p. 8). (6) Iterate until there are no goals and the kernel accepts the theorem; otherwise classify it as incomplete. The paper summarizes the interaction: “The persistent Lean REPL serves as an interactive interface for stepwise proof construction: the agent submits a proof step, inspects the resulting goals and diagnostics, and selects or revises the next step.” (Appendix E, p. 24.)

Verus form. Inference: define a spec fn for the mathematical behavior, put preconditions on executable Rust with requires, and prove equality or refinement with a proof fn and ensures; use old(...) when relating pre-state values and loop invariant clauses for induction. Do not call proof functions at runtime. Inference: Verus has no persistent Lean REPL, so the practical loop is edit–run verus–read diagnostics–edit; a failing proof obligation is analogous to a residual Lean goal. The theorem’s explicit reset assumptions should become requires, not hidden comments.

Evidence. On 30 VerilogEval problems, one-shot generation produced compile 77%, simulation 50%, kernel proof 16/30 (53.3%), and Yosys equivalence 70%; stepwise feedback produced compile 100%, simulation 70%, kernel proof 19/30 (63.3%), and Yosys equivalence 73% (Section 5.3, pp. 8–9). The proof denominator is 30 in both modes. The paper gives the conclusion precisely: “Stepwise proof development improves all metrics, raising compile pass from 77% to 100%, simulation from 50% to 70%, kernel-accepted proof completion from 53.3% (16/30) to 63.3% (19/30), and Yosys equivalence from 70% to 73%.” (Section 5.3, p. 9.)

Failure and assumptions. A completed proof establishes only the stated source-level property; it does not establish that the formal specification faithfully captures natural language (Appendix E, p. 24). Proof automation is design-dependent; sequential designs may need extra lemmas or induction (Appendix E, p. 25). Inference: this is a direct threat boundary for agent-written verified Rust: a green Verus proof can still certify the wrong contract.

technique 3: independent RTL equivalence and simulation evidence

What it is. The pipeline checks emitted SystemVerilog separately from Lean source proofs. Yosys combines SAT-based combinational reasoning (equiv_simple) with sequential induction (equiv_induct) to compare generated RTL with a benchmark reference (Appendix E, p. 25). RTL simulation checks finite testbench traces.

How to apply it. (1) Extract SystemVerilog from the typed source. (2) Run linting and reference-testbench simulation. (3) Run Yosys equivalence against the reference RTL using the configured combinational and sequential procedures. (4) Run synthesis, place-and-route, DRC, and LVS when backend realizability is required. (5) Keep the evidence categories separate: simulation covers exercised traces, Yosys covers its model and procedure, and Lean covers source definitions. The paper states: “A central verification boundary lies between the Lean source semantics and the emitted SystemVerilog.” (Appendix E, p. 25.)

Verus form. Inference: Verus can prove the Rust-level contract, while a separate executable test, model checker, or equivalence checker would be needed for generated machine code or FFI behavior. Verus does not provide CKTLEAN’s HDL extraction or Yosys integration. Inference: if VL emits Rust that calls unverified libraries, treat those calls like the paper treats the source-to-RTL compiler boundary and record them as trusted assumptions.

Evidence and limits. Table 9 says Lean kernel proofs apply within the formal signal model, Yosys is limited by supported constructs and configured procedures, and “Simulation covers only the exercised inputs and time horizon, while RTL equivalence remains tool- and design-dependent.” (Section 4.1, p. 4.) The paper explicitly reports no end-to-end compiler-correctness proof: “Neither directly establishes that the Lean-to-SystemVerilog translation preserves the source semantics.” (Appendix E, p. 25.) Timing-aware or gate-level equivalence and post-synthesis parasitics are outside scope (Appendix E, p. 25).

technique 4: synthesis-feedback PPA optimization with proof preservation

What it is. The agent iteratively modifies a selected implementation using measured area, power, timing slack, and cell count. A candidate is retained only if it passes configured checks and improves at least one normalized metric without excessive degradation in another (Section 4.2, pp. 5–6).

How to apply it. (1) Generate C architectural candidates and compare them; the default is C=3, while the VerilogEval optimization experiment uses C=4 (Section 4.2, p. 5; Section 5.3, p. 9). (2) Select the best simulation-passing seed. (3) Run K iterations (default K=3; reported experiment K=5), giving the agent metric history and bottleneck guidance. (4) Modify Lean source, recompile, simulate, and synthesize. (5) Normalize each metric change and accept only if one improves by more than τ and no metric degrades by more than ε; otherwise roll back (Equation 1, Section 4.2, p. 6). (6) Prove equivalence between original and revised designs when correctness-preserving optimization is required.

Verus form. Inference: use a benchmark harness that proposes Rust refactorings, runs verus, and measures runtime or resource metrics; preserve a proof obligation relating old and new behavior. Use a separate candidate acceptance script because Verus proves contracts but does not measure PPA. Inference: the paper’s rollback rule maps to retaining only candidates that pass verification and satisfy explicit metric thresholds.

Evidence. In the 63-problem VerilogEval subset, 54 designs entered the loop, 31 changed Lean and reduced Yosys area, and 28 exceeded the 5% threshold; the largest reported reduction was 58.6% (196 to 81 µm²) (Section 5.3, p. 9). Six illustrative simulation-passing designs reduced area by 9.9%–35.2%, cell count by 0.0%–45.9%, and power by 2.0%–30.3% (Table 4, p. 9). A separate tight-clock pass improved one design’s setup slack from −0.37 ns to +0.35 and +0.31 ns (Section 5.3, p. 9). These are selected examples and do not establish universal optimization gains.

Failure and assumptions. The area-focused loop leaves timing at −0.37 ns in the reported case (Section 5.3, p. 9). Inference: optimizing one metric while merely preserving type correctness can make a product worse on unmeasured resource or timing dimensions. The acceptance thresholds, normalization floors, and benchmark setup are trusted parts of the experiment.

what is proved, measured, and trusted

Lean type checking proves supported structural invariants; kernel proofs prove stated source properties; Yosys checks emitted-RTL equivalence under its assumptions; simulation measures finite traces; synthesis and physical design measure realizability. The paper’s own boundary statement is: “Completed Lean theorems establish the source-level functional properties they state.” (Appendix E, p. 25.)

Inference: trusted components include the natural-language specification, theorem statements, CKTLEAN semantics and compiler, Lean kernel, Yosys models, reference RTL/testbenches, synthesis tools, and assumptions about clocks, reset, libraries, and hardware. The paper does not prove compiler correctness from Lean signals to SystemVerilog, nor semantic correctness of the natural-language requirement. For VL, the highest product threat is specification/API error hidden behind a successful proof; the most reusable mitigation is a staged loop that exposes compiler/proof state and independently checks generated artifacts.

Inference: VL should not redo the paper’s generic insight that interactive verifier feedback helps proof search. A potentially useful extension is to measure whether the same loop repairs Verus API and contract design, because this paper evaluates hardware generation and Lean proof steps rather than Rust systems APIs.

techniques for the catalog

• typed intermediate representation and compiler-guided repair — encode structural invariants in types, then repair from persistent compiler diagnostics before extraction
• stepwise proof-state-guided equivalence — iterate proof steps against residual goals until the kernel accepts a no-placeholder theorem
• independent artifact checking — combine source proofs with RTL equivalence, finite simulation, and physical-design checks while recording each scope
• synthesis-feedback optimization with proof preservation — accept measured improvements only after recompilation/evaluation and preserve behavior with an equivalence proof Checked 2026-10-14 against the paper by a Codex agent: audit record xiong2026cktformalizer; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15