Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse

Hongqin Lyu; Huawei Li; Junxing Dong; Tiancheng Wang; Yonghao Wang; Zhiteng Chao

REVIEW 2 major objections 5 minor 13 references

Rtl2lean automatically translates SystemVerilog RTL into Lean 4 models and reports 403 machine-checked theorems across six designs.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 19:43 UTC pith:SPJPLUDB

load-bearing objection Useful RTL-to-Lean translator with a real semantic-fidelity gap; the LLM loop is not actually evaluated. the 2 major comments →

arxiv 2607.16855 v1 pith:SPJPLUDB submitted 2026-07-18 cs.AR cs.LO

Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse

Hongqin Lyu , Junxing Dong , Yonghao Wang , Zhiteng Chao , Tiancheng Wang , Huawei Li This is my paper

classification cs.AR cs.LO

keywords RTL verificationLean 4SystemVerilogtheorem provingLLM-assisted prooflemma reuseformal hardware verification

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Rtl2lean is an attempt to remove the manual bottleneck that has kept interactive theorem proving out of reach for ordinary RTL designs: instead of asking a human to model SystemVerilog in Lean and construct proofs, the framework compiles the RTL directly into a pure state-transition function and then auto-generates a layered library of lemmas about that function. High-level properties are proved by reusing this library; when the library is insufficient, an LLM proposes candidate intermediate lemmas, and only those that pass the Lean kernel are added to the reusable pool. On six designs the paper reports 403 generated theorems, every one accepted by Lean, with 287 of 358 foundational lemmas available for automatic reuse (80.2%). The reader should care because, if correct, this turns machine-checked verification from a hand-crafted speciality into a push-button step that runs in about a second per design, complementing simulation and model checking rather than replacing them.

Core claim

The central claim, stated in the paper's own terms, is that a syntax-directed RTL-to-Lean compiler plus a fixed theorem skeleton can generate, for any SystemVerilog design, a formal model whose properties are largely provable by simplification. The framework encodes the whole design's behavior as a pure function step(s,i) returning the next state, then builds four layers of theorems — combinational semantics and preservation, sequential update behavior, single-cycle step behavior, and reachability/invariants. When a target property cannot be discharged by these layers, the framework enters a generate–check–repair loop in which an LLM proposes lemmas from the proof context and Lean error feed

What carries the argument

The load-bearing machinery is the single-cycle transition function step(s,i): a pure functional encoding of the whole RTL design that returns the next state. Around it the framework generates a bottom-up four-layer theorem library — combinational semantic/preservation lemmas, sequential-update determinism/preservation lemmas, step-level reset/transition/output theorems, and reachability/invariant theorems — so that high-level proofs reduce to simplification over already-proved lemmas. The second piece is the Lean-guided LLM loop: the proof context and Lean error messages drive generation of candidate lemmas, and acceptance by the Lean kernel is the sole criterion for adding a lemma to the re

Load-bearing premise

The load-bearing premise is that the generated step function reproduces, at the level of clock cycles, exactly what the original SystemVerilog design does; Lean only checks theorems about the generated model, so any translation error would make all 403 theorems true of a model that is not the hardware.

What would settle it

A concrete falsifier would be one SystemVerilog design or test case where Rtl2lean's generated step function disagrees with a standard event-driven simulator on some input sequence — for example, a pair of always_ff blocks with overlapping writes, or a blocking assignment used in a combinational process where read-after-write order matters. If a golden simulation produces a different next-state than evaluating step(s,i) in Lean on the same inputs, the translation-faithfulness claim is refuted even though every Lean theorem checks. A direct check would be to run trace comparison on the six repo

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

Interactive verification of existing RTL no longer has to start from a hand-written semantic model: the compiler produces the model and its proof skeleton automatically from SystemVerilog.
The low runtimes reported (0.65s generation, 5.57s checking for all six designs) make the flow fast enough to re-run on every RTL revision.
Because only kernel-accepted lemmas enter the pool, later proofs are built on verified premises, and the 80.2% reuse ratio indicates most foundational results are applied automatically by the simplifier.
The reachability and invariant layer lifts properties from single cycles to arbitrary-length executions, covering behaviors that finite simulation cannot exhaustively check.
The method targets existing RTL rather than requiring designs to be written in a proof-friendly language, addressing the main adoption barrier of previous theorem-prover-based hardware verification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the 100% proof-success rate measures the generated library and template instantiations, not the difficulty of arbitrary hardware proofs; the actual hard problem is pushed into translation faithfulness and into the choice of high-level properties.
Editorial inference: an obvious stress test for the framework is to apply it to RTL using event-driven scheduling, multiple always blocks with inter-dependent assignments, latches, x-values, or asynchronous resets; the six benchmarks are small synchronous designs, so the cycle-level abstraction may not cover those constructs.
Editorial inference: the reusable-lemma ratio is a measure of availability, not actual dynamic usage, so comparing cross-design proof reuse should be done with care; a stronger metric would count how many times each lemma discharges a goal across a held-out property set.
Editorial inference: because all LLM output is kernel-gated, better or worse LLMs affect lemma-discovery coverage but cannot corrupt the theorem base; the scalability bottleneck is likely the translation front-end and the theorem-template coverage, not proof search.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

Useful RTL-to-Lean translator with a real semantic-fidelity gap; the LLM loop is not actually evaluated.

read the letter

Honestly, the interesting part of this paper is the translator, not the theorem prover integration. The idea of parsing SystemVerilog, lowering to an IR, and emitting a pure `step` function in Lean is genuinely useful and I don't know of another tool that does that for existing RTL. The four-layer theorem framework is a reasonable way to structure proofs, and the 403 machine-checked theorems are real, as far as they go. The reusable lemma ratio is a sensible metric.

Where it gets shaky is the connection between the Lean model and the actual SystemVerilog. The paper asserts in §III-A that the generated `step` 'faithfully preserves the cycle-level semantics of the original design,' but it never defines what that means formally, never proves that the PySlang-to-IR-to-Lean pipeline preserves anything, and reports no simulation or equivalence check. Lean checking only tells you the proofs are valid about the model; it says nothing about whether the model matches the RTL. That's a missing-evidence problem, not evidence of unsoundness, but it is the load-bearing claim and the weakest part of the paper.

Also, the LLM-assisted proof loop is not actually evaluated. The paper says in Section IV-D that the deterministic proof templates require no external model calls and T_e2e is only 0.650 seconds. So the 'LLM-assisted' part is a proposal, not a result. The 100% proof success rate is for template-generated proofs on six small OpenCores designs. That is a fine demonstration of the translator, but it does not support the conclusion about LLM lemma generation. No artifact is shipped, no baseline comparison, no counterexamples.

The authors do give a clear explanation of the framework, and the generated examples look plausible. For someone building RTL-to-proof-assistant tooling, this is worth reading. But the effectiveness claims need to be reined in until the semantic fidelity is validated and the LLM loop is actually run.

Recommendation: send to peer review, but flag that the semantic-preservation claim needs either a formal proof or at least equivalence checking against simulation, and the experimental section should clearly separate what is actually exercised from what is hypothetical.

Referee Report

2 major / 5 minor

Summary. The paper presents Rtl2lean, a framework that translates SystemVerilog RTL into an executable Lean 4 state-transition model and automatically generates a four-layer theorem library (combinational lemmas, sequential-block lemmas, step-level theorems, and reachability/invariants). A third component is an LLM-guided proving loop that proposes intermediate lemmas in response to Lean feedback, admits only kernel-checked lemmas into a reusable pool, and uses them in later proofs. Experiments on six OpenCores designs report 403 generated theorems, all checked by Lean, with a 100% proof success rate, an 80.2% reusable-lemma ratio, and low checking time.

Significance. If the claims hold, Rtl2lean would provide a useful bridge from existing SystemVerilog RTL to machine-checked Lean proofs, with meaningful automation of the notoriously labor-intensive steps of semantic modeling and proof construction. The reported artifacts are machine-checked by the Lean kernel, so the 403 theorems are valid with respect to the generated model, and the four-layer structured theorem library is a reasonable way to reduce repeated low-level reasoning. However, the significance is conditional on two unaddressed points: the semantic fidelity of the RTL-to-Lean translation, and the actual evaluation of the LLM-based lemma-generation loop. The paper's own experiment text states that the proof pipeline used no external model calls, so the empirical support for the headline LLM contribution is currently absent. The work is a solid prototype, but the evidence as presented does not yet establish the full claimed end-to-end guarantee.

major comments (2)

[§III-A] The central load-bearing claim is that the generated `step` function 'faithfully preserves the cycle-level semantics of the original design.' This is asserted, not demonstrated. There is no formal definition of 'cycle-level semantics,' no proof of semantic preservation for the PySlang→IR→Lean lowering, and no empirical equivalence check against a simulation reference or a formal SystemVerilog semantics. Lean kernel checking only establishes theorems about the generated model; it cannot detect translation errors for constructs such as non-blocking-assignment timing, event-driven scheduling, width/overflow behavior, or combinational loops. I recommend the authors provide a concrete artifact: a supported-SystemVerilog-subset specification, a simulation cross-check (e.g., randomized differential testing against Verilator or Icarus), or a proof of semantic preservation for the supported const
[§IV-D and §III-C] The experiment does not exercise the LLM-based proving loop described in §III-C and highlighted in the abstract. Section IV-D states that the end-to-end time is only 0.650 s 'since the deterministic proof templates require neither proof search nor external model calls.' Consequently, the 403 theorem results come entirely from template generation, not from the generate–check–repair loop of Eq. (9) or from LLM-proposed intermediate lemmas. No data are reported on LLM proposal counts, acceptance rates, repair iterations, or a comparison with/without the lemma pool. Thus the paper's second contribution—LLM-assisted lemma generation and reuse—is untested by the experiments. The authors should either evaluate the LLM loop on high-level properties that require non-template lemmas, or revise the abstract and contribution claims to separate the template-generated library from the LLM-assisted ext

minor comments (5)

[§IV-B] The text says 'We additionally report the numbers of errors, unresolved goals, and proofs containing sorry,' but Table III does not include these columns. Since the 100% success rate is a headline result, reporting these counts explicitly would strengthen the claim.
[§IV-A] There are typos in the section header: 'Expermental' should be 'Experimental' in both the section title and the 'Expermental set' heading.
[Throughout] Notation is inconsistent: the tool is written as `rtl2lean`, `Rtl2lean`, and `RTL2LEAN` in different places (e.g., §III-A, Fig. 1 caption, §IV). Please standardize.
[§IV-A / Table I] The six OpenCores designs are named but no repository URLs, commits, revisions, or configuration parameters are given. This makes the experimental artifacts not reproducible from the paper alone. Please provide precise design versions or an artifact link.
[§IV-B, Eq. (13)] The reusable-lemma ratio is defined as the proportion of foundational lemmas 'available for automatic reuse,' not the proportion actually used in proofs. The paper does state this caveat, but the headline '80.2% reusable lemma ratio' could be read as measured dynamic reuse. I suggest renaming the metric or reporting both availability and actual usage.

Circularity Check

0 steps flagged

No significant circularity: the Lean-generated proofs are machine-checked against the framework's own model; the unproven RTL-semantic-fidelity claim is a validation gap, not a circular derivation.

full rationale

The paper's derivation chain is not circular. Rtl2lean parses SystemVerilog with PySlang, lowers it to an intermediate representation, and generates a pure Lean 4 step function; the four-layer theorem framework is then generated from that model, and high-level properties are proved about it. The Lean kernel check is an independent mechanical validator for every generated proof, so the reported 403 theorems are genuinely checked relative to the framework's definitions. The load-bearing claim of semantic fidelity to the original SystemVerilog (§III-A, 'faithfully preserving the cycle-level semantics of the original design') is asserted rather than proved, and no simulation or equivalence check is reported; however, this is a missing-evidence/external-validity threat, not circularity, because the Lean model is not defined in terms of the target properties and no equation reduces the RTL semantics to the generated model or vice versa. No load-bearing self-citation, imported uniqueness theorem, or ansatz-by-citation appears. The LLM lemma loop was not exercised in the timing experiments (Section IV-D says deterministic templates require no external model calls), which is an evaluation inconsistency rather than a circular step. One minor internal-metric ambiguity exists: N_total is described as 'generated and checked by Lean' in Section IV-B, which would make Eq. (12)'s 100% success rate tautological; the immediately following prose says N_total is the total number of generated theorems, so I do not treat this as a demonstrated circular reduction. Overall, the core formal artifacts are self-consistently Lean-checked and the central derivation is not circular.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

The paper introduces no fitted numerical parameters and no new physical or mathematical entities. Its load-bearing assumptions are about semantic fidelity of the RTL-to-Lean compiler, the meaningfulness of the generated properties, and the untested utility of the LLM loop. The Lean kernel supplies logical soundness but not hardware semantic soundness.

axioms (5)

domain assumption The generated Lean function `step` faithfully captures SystemVerilog cycle-level semantics.
Invoked in §III-A to justify the translation; no proof or equivalence validation against IEEE 1800 semantics, so all formal results inherit this unverified assumption.
domain assumption The high-level properties verified are meaningful correctness requirements for the original designs.
Properties are presented as outputs of the pipeline; the paper does not show they are independently derived from specifications rather than inferred from the implementation, so a trivial theorem set would still score 100%.
standard math Lean 4 kernel is sound and its standard definitions used are correct.
Standard assumption for any proof-assistant-based result.
domain assumption LLM-generated lemma candidates accepted by the Lean kernel advance proofs and are semantically useful.
The loop is described in §III-C but not evaluated; kernel checking ensures logical validity, not usefulness or semantic relevance.
ad hoc to paper The four-layer theorem templates cover all proof obligations needed for realistic RTL properties.
Framework design choice in §III-B; generalization beyond six small benchmarks is untested.

pith-pipeline@v1.3.0-alltime-deepseek · 6984 in / 10201 out tokens · 103094 ms · 2026-08-01T19:43:36.274181+00:00 · methodology

0 comments

read the original abstract

Formal verification with interactive theorem provers can provide strong correctness guarantees for register transfer level designs, but applying it to existing SystemVerilog code requires substantial manual effort in semantic modeling and proof construction. This paper presents Rtl2lean, a framework that automatically translates RTL designs into executable Lean 4 models and builds a hierarchical theorem library for subsequent verification. The generated model represents hardware execution as a pure state transition function, while a four layer theorem framework captures combinational semantics, sequential updates, single cycle behavior, and reachability and invariants. When a high level property cannot be discharged by the existing theorem base, an LLM based proving loop proposes intermediate lemmas from the current proof context and Lean feedback. Only lemmas accepted by the Lean kernel are added to the reusable lemma pool. Experiments on six SystemVerilog designs generate 403 theorems, all of which are successfully checked by Lean. Among 358 foundational lemmas, 287 are available for automatic reuse, yielding a reusable lemma ratio of 80.2 percent. The results demonstrate that Rtl2lean can construct machine checked RTL proof libraries with low checking overhead and substantial cross property lemma reuse.

Figures

Figures reproduced from arXiv: 2607.16855 by Hongqin Lyu, Huawei Li, Junxing Dong, Tiancheng Wang, Yonghao Wang, Zhiteng Chao.

**Figure 1.** Figure 1: RTL2LEAN framework. representation, where conditional updates are normalized as selection expressions and different assignment types retain their corresponding update semantics. After standard optimizations, such as constant folding, dead-code elimination, and common-subexpression elimination, the backend generates a Lean 4 model consisting of State, Inputs, Outputs, and a single-cycle transition function… view at source ↗

**Figure 2.** Figure 2: Representative examples generated by the four-layer. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 2 linked inside Pith

[1]

Trends in functional verification: A 2014 industry study,

H. D. Foster, “Trends in functional verification: A 2014 industry study,” inProceedings of the 52nd Annual Design Automation Conference, ser. DAC ’15. New York, NY , USA: Association for Computing Machinery, 2015, pp. 48:1–48:6

2014
[2]

E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds.,Handbook of Model Checking. Cham: Springer, 2018

2018
[3]

Symbolic model checking without BDDs,

A. Biere, A. Cimatti, E. M. Clarke, and Y . Zhu, “Symbolic model checking without BDDs,” inTools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science, W. R. Cleaveland, Ed., vol. 1579. Berlin, Heidelberg: Springer, 1999, pp. 193–207

1999
[4]

Model checking and the state explosion problem,

E. M. Clarke, W. Klieber, M. Nov ´aˇcek, and P. Zuliani, “Model checking and the state explosion problem,” inTools for Practical Software Verification, ser. Lecture Notes in Computer Science, B. Meyer and M. Nordio, Eds. Berlin, Heidelberg: Springer, 2012, vol. 7682, pp. 1–30

2012
[5]

The Lean 4 theorem prover and pro- gramming language,

L. de Moura and S. Ullrich, “The Lean 4 theorem prover and pro- gramming language,” inAutomated Deduction – CADE 28, ser. Lecture Notes in Computer Science, A. Platzer and G. Sutcliffe, Eds., vol. 12699. Cham: Springer, 2021, pp. 625–635

2021
[6]

Kami: A platform for high-level parametric hardware specification and its modular verification,

J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvind, “Kami: A platform for high-level parametric hardware specification and its modular verification,”Proceedings of the ACM on Programming Languages, vol. 1, no. ICFP, pp. 24:1–24:30, 2017

2017
[7]

Silver Oak: Formal specification and verification of hard- ware,

Project Oak, “Silver Oak: Formal specification and verification of hard- ware,” https://project-oak.github.io/silveroak/, accessed: 2026-07-17

2026
[8]

IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language,

IEEE, “IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language,” Institute of Electrical and Electronics Engineers, New York, NY , USA, IEEE Standard IEEE Std 1800-2023, Feb. 2024, revision of IEEE Std 1800-2017

2023
[9]

Generative language modeling for automated theorem proving,

S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”arXiv preprint arXiv:2009.03393, 2020

Pith/arXiv arXiv 2009
[10]

LeanDojo: Theorem proving with retrieval-augmented language models,

K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “LeanDojo: Theorem proving with retrieval-augmented language models,” inAdvances in Neural Informa- tion Processing Systems, vol. 36. Curran Associates, Inc., 2023, pp. 21 573–21 612

2023
[11]

CktFormalizer: Autoformalization of natural language into circuit rep- resentations,

J. Xiong, Q. Han, C. Ding, H. Xiao, Z. Su, C. Tao, and N. Wong, “CktFormalizer: Autoformalization of natural language into circuit rep- resentations,”arXiv preprint arXiv:2605.07782, 2026

Pith/arXiv arXiv 2026
[12]

OpenCores: Free and open-source gateware IP cores,

OpenCores, “OpenCores: Free and open-source gateware IP cores,” https://opencores.org/, online resource, accessed July 18, 2026

2026
[13]

Lean 4.26.0 release notes,

Lean FRO, “Lean 4.26.0 release notes,” https://lean- lang.org/doc/reference/latest/releases/v4.26.0/, Dec. 2025, released December 13, 2025; accessed July 18, 2026

2025

[1] [1]

Trends in functional verification: A 2014 industry study,

H. D. Foster, “Trends in functional verification: A 2014 industry study,” inProceedings of the 52nd Annual Design Automation Conference, ser. DAC ’15. New York, NY , USA: Association for Computing Machinery, 2015, pp. 48:1–48:6

2014

[2] [2]

E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds.,Handbook of Model Checking. Cham: Springer, 2018

2018

[3] [3]

Symbolic model checking without BDDs,

A. Biere, A. Cimatti, E. M. Clarke, and Y . Zhu, “Symbolic model checking without BDDs,” inTools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science, W. R. Cleaveland, Ed., vol. 1579. Berlin, Heidelberg: Springer, 1999, pp. 193–207

1999

[4] [4]

Model checking and the state explosion problem,

E. M. Clarke, W. Klieber, M. Nov ´aˇcek, and P. Zuliani, “Model checking and the state explosion problem,” inTools for Practical Software Verification, ser. Lecture Notes in Computer Science, B. Meyer and M. Nordio, Eds. Berlin, Heidelberg: Springer, 2012, vol. 7682, pp. 1–30

2012

[5] [5]

The Lean 4 theorem prover and pro- gramming language,

L. de Moura and S. Ullrich, “The Lean 4 theorem prover and pro- gramming language,” inAutomated Deduction – CADE 28, ser. Lecture Notes in Computer Science, A. Platzer and G. Sutcliffe, Eds., vol. 12699. Cham: Springer, 2021, pp. 625–635

2021

[6] [6]

Kami: A platform for high-level parametric hardware specification and its modular verification,

J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvind, “Kami: A platform for high-level parametric hardware specification and its modular verification,”Proceedings of the ACM on Programming Languages, vol. 1, no. ICFP, pp. 24:1–24:30, 2017

2017

[7] [7]

Silver Oak: Formal specification and verification of hard- ware,

Project Oak, “Silver Oak: Formal specification and verification of hard- ware,” https://project-oak.github.io/silveroak/, accessed: 2026-07-17

2026

[8] [8]

IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language,

IEEE, “IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language,” Institute of Electrical and Electronics Engineers, New York, NY , USA, IEEE Standard IEEE Std 1800-2023, Feb. 2024, revision of IEEE Std 1800-2017

2023

[9] [9]

Generative language modeling for automated theorem proving,

S. Polu and I. Sutskever, “Generative language modeling for automated theorem proving,”arXiv preprint arXiv:2009.03393, 2020

Pith/arXiv arXiv 2009

[10] [10]

LeanDojo: Theorem proving with retrieval-augmented language models,

K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar, “LeanDojo: Theorem proving with retrieval-augmented language models,” inAdvances in Neural Informa- tion Processing Systems, vol. 36. Curran Associates, Inc., 2023, pp. 21 573–21 612

2023

[11] [11]

CktFormalizer: Autoformalization of natural language into circuit rep- resentations,

J. Xiong, Q. Han, C. Ding, H. Xiao, Z. Su, C. Tao, and N. Wong, “CktFormalizer: Autoformalization of natural language into circuit rep- resentations,”arXiv preprint arXiv:2605.07782, 2026

Pith/arXiv arXiv 2026

[12] [12]

OpenCores: Free and open-source gateware IP cores,

OpenCores, “OpenCores: Free and open-source gateware IP cores,” https://opencores.org/, online resource, accessed July 18, 2026

2026

[13] [13]

Lean 4.26.0 release notes,

Lean FRO, “Lean 4.26.0 release notes,” https://lean- lang.org/doc/reference/latest/releases/v4.26.0/, Dec. 2025, released December 13, 2025; accessed July 18, 2026

2025