Pith. sign in

REVIEW 3 major objections 5 minor 50 references

CircuitProver claims that an LLM-driven Lean 4 agent, augmented with a reusable proof library, can automatically construct machine-checked correctness proofs for parameterized hardware designs, and demonstrates this on all 63 benchmark task

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 15:47 UTC pith:3FPK53JV

load-bearing objection A genuinely useful benchmark and proof-library mechanism for agentic hardware verification, but the all-width guarantee is weaker than the abstract implies. the 3 major comments →

arxiv 2607.27259 v1 pith:3FPK53JV submitted 2026-07-29 cs.LO cs.AR

CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification

Ziyi Yang , Wenji Fang , Chen Chen , Zhiyao Xie , Hongce Zhang This is my paper
classification cs.LO cs.AR
keywords agentic theorem provinghardware verificationLean 4proof reuseparameterized verificationChiselformal verificationLLM agents
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.

This paper tries to establish that hardware verification can be reorganized around reusable, machine-checked proof knowledge instead of one-off model-checking runs. It presents CircuitProver, an agent that translates parameterized Chisel designs and natural-language specs into Lean 4 models, then iteratively builds proofs from Lean feedback. The agent's successful proof traces are distilled into two libraries: natural-language proof guidance and module-independent verified theorems. On a new 63-task benchmark of arithmetic, control, memory, and miscellaneous circuits, the system proves every task, while a matched vanilla agent solves 92.1% and needs roughly twice as many proof rounds. A sympathetic reader would care because a single parameterized proof can cover an entire family of circuit instances, and the accumulated lemmas carry over to related designs.

Core claim

CircuitProver claims that parameterized hardware correctness can be fully automated as agentic Lean 4 theorem proving with knowledge accumulation. A deterministic translator maps Chisel designs into executable Lean models that keep parameters symbolic; the agent formulates the specification, plans a hardware-aware proof scaffold (one-step transition lemmas and inductive invariants for sequential circuits), and repairs proof scripts against Lean's errors until the kernel accepts. Successful trajectories are then distilled: proof strategies go into a guidance library, and decoupled, module-independent theorems go into a checked library. In the paper's evaluation, this setup proves all 63 bench

What carries the argument

The load-bearing mechanism is proof accumulation through a two-part reusable library. The Lean-Checked Theorem Library stores decoupled, module-independent lemmas—for example, a fold closure theorem that lifts block-level sum-and-carry relations to full-width correctness—so future tasks can instantiate the same fact instead of re-deriving it. The Proof Guidance Library records the reasoning route: which lemma to apply, how to decompose the proof, and how to repair representation-level failures. Together they turn the agent's successful trajectory into a reusable asset, which is what lets a single verified proof of a carry-skip adder transfer to other blocked adders that share the one-block s

Load-bearing premise

The whole result rests on the Chisel-to-Lean translator preserving the design's execution behavior for every parameter value; the paper validates this only by exhaustive co-simulation at small bit widths, not by a semantic-equivalence proof.

What would settle it

Pick a benchmark design and simulate the original Chisel circuit and its generated Lean model at a bit width outside the small configurations used for validation (say n=64 or n=128). If any input sequence produces different outputs, the translator is not semantics-preserving, and the Lean theorem can be true while the hardware is wrong. A width-dependent divergence would directly undercut the soundness of the claimed verification.

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

If this is right

  • A single verified Lean theorem can establish correctness for all parameter values of a design generator, not just one instantiated width.
  • Verified lemmas and proof strategies transfer across related designs, so succeeding verification tasks become cheaper: the paper reports 16.3% shorter proofs and 23.2% less verification time on average.
  • The advantage grows with design size: on four processor-level arithmetic modules, the paper reports reductions of roughly 48–57% in proof rounds, time, tokens, and proof length versus a vanilla agent.
  • The agent's success scales with the underlying language model's capability: coverage in the paper rises from 31/63 to 63/63 across four models.
  • The benchmark's Lean-level evaluation interface means the approach is not tied to Chisel as the source language; other design frontends could feed the same proving workflow.

Where Pith is reading between the lines

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

  • Looking beyond the paper, if translator semantic preservation holds for all widths, verification practice could shift toward proofs as durable assets—each verified design family enriches the next rather than disappearing into a pass/fail result.
  • A plausible extension is to apply the same accumulation loop to other generator-based domains, such as software templates or configurable IP blocks, where instances share structure but differ in parameters.
  • A testable follow-up would measure whether the library's value keeps compounding as the task set grows: does marginal cost per new design keep falling, and does it plateau without higher-level structural abstractions?
  • An open direction the paper leaves implicit is replacing co-simulation validation with a verified translator, which would remove the residual gap between the Lean theorem and the original hardware semantics.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. CircuitProver is an agentic Lean 4 verification framework for parameterized Chisel hardware. It translates Chisel designs and natural-language specifications into executable Lean 4 models, uses an LLM-based agent to iteratively construct machine-checked proofs, and distills successful proof trajectories into a reusable proof-guidance library and a Lean-checked theorem library. The paper introduces a 63-task benchmark of parameterized hardware verification problems and reports that CircuitProver proves all 63 tasks, outperforming a vanilla agent (92.1% solved) with fewer proof rounds, lower proof LoC, and reduced verification time. Ablations show that both the theorem library and proof guidance contribute to coverage and convergence speed.

Significance. If the soundness concerns are resolved, this is a useful contribution to the emerging area of LLM-driven interactive theorem proving for hardware. The machine-checked nature of the Lean proofs, the public-style benchmark, and the systematic ablations are strengths. The central claim, however, depends on an unproven semantic bridge: the Chisel-to-Lean translator is only finitely validated by small-bit-width co-simulation, and the formal specifications are themselves validated against the implementation. Thus the reported '63/63 proved' certifies machine-checked consistency among generated artifacts, not necessarily correctness of the original Chisel designs. This limits the significance of the headline result until the translation/specification soundness is established or the claims are scoped more modestly.

major comments (3)
  1. [Phase I (Eq. (3))] The translator T_impl is claimed to produce an executable Lean model that preserves the original design's behavior, and the paper's headline is parameterized verification 'for all widths.' However, the only validation offered is 'exhaustive small-bit-width co-simulation... for the evaluated bit-width configurations.' A finite test on small widths does not certify semantic equivalence for arbitrary n. A width-dependent translation bug (e.g., in overflow, truncation, or bit-vector width arithmetic) would make the Lean theorem true while the Chisel hardware violates the specification. The paper must either provide a formal proof of translation correctness for the supported Chisel subset, or explicitly restrict the claimed theorem to the generated Lean model rather than the original Chisel design. As written, the soundness of the central 'parameterized verification' claim is not established.
  2. [Step 1 (Eq. (4), Eq. (5))] The formal specification L_S is generated by an LLM from natural language and hardware context, then 'validated using the same exhaustive small-bit-width co-simulation procedure as in Phase I.' This validation is against the implementation, so it does not independently establish that L_S captures the intended behavior; it only shows agreement on small instances. Consequently, proving L_D satisfies L_S is not a verification of the hardware against an independent specification. The paper should provide a way to validate the formal specification that is not grounded in the implementation it is meant to check, or clearly state that the theorem certifies consistency between the generated model and the generated specification. As is, this is a circularity in the verification argument.
  3. [Experiment / Table 1] The abstract and conclusion state that CircuitProver 'successfully proves all benchmarks.' This is true only for the Lean models and specifications produced by the tool's own pipeline, not necessarily for the original Chisel designs, given the two issues above. The paper should precisely delineate the claim: what is machine-checked is a theorem about L_D and L_S. Without such a qualification, readers may over-interpret the result as verification of Chisel RTL. This is a presentation/scoping issue, but it is load-bearing for the paper's contribution.
minor comments (5)
  1. [Section 3] Typo: 'introduing' should be 'introducing' in the benchmark-section preamble.
  2. [Figure 2] In the Lean code snippet, 'Bitvec' appears with inconsistent capitalization; it should be 'BitVec' to match the text.
  3. [References] Several reference entries have missing spaces or formatting glitches (e.g., 'Moura, L.d.; and Ullrich, S. 2021. Thelean4theoremprover'). Please normalize.
  4. [Table 1] The footnotes use unusual symbols (‡, ♢) that are not defined in the caption. Please clarify what 'Chicala/Stainless' and the diamond denote, and state explicitly that time/LoC/token/round averages are computed over different solved-task subsets.
  5. [General] If a benchmark artifact or code release is available, a link should be provided; otherwise state availability explicitly.

Circularity Check

1 steps flagged

Specification is generated from the implementation and validated by co-simulation against it, so the 63/63 proofs certify consistency among aligned artifacts rather than independent compliance.

specific steps
  1. fitted input called prediction [Methodology, Phase II, Step 1 (Specification Formulation), Eq. (4)-(5); Phase I co-simulation paragraph]
    "Given the transformed Lean hardware model L_D and its natural-language specification S, the reasoning agent analyzes the circuit structure and formulates the corresponding Lean 4 specification L_S. ... We validate the formalized specifications using the same exhaustive small-bit-width co-simulation procedure as in Phase I."

    The Lean specification L_S is produced by F_spec from the Lean implementation L_D and then validated by co-simulation against the implementation. The formal specification is therefore derived from and filtered by the very design it is supposed to constrain. The theorem Phi(L_D, L_S) then certifies consistency between two artifacts that were explicitly aligned, not an independent check of the hardware against the natural-language intent. The all-width Lean proof is still nontrivial and machine-checked, so this is partial circularity rather than a tautology.

full rationale

The central formal result is a Lean-checked proof of Phi(L_D, L_S), where L_D is generated by the Chisel-to-Lean translator and L_S is generated by the agent from L_D plus the natural-language spec. The paper explicitly validates L_S with the same exhaustive small-bit-width co-simulation used to validate L_D, meaning the specification's semantic content is anchored in the implementation's observed behavior. This compromises the claim that the benchmarks demonstrate hardware compliance with an independent specification: the 63/63 success rate shows that the generated Lean model and the generated Lean spec agree, for all widths, under a proof that the agent was able to construct. The proof itself is genuine and not forced by the co-simulation, so the circularity is partial. Separately, the soundness of T_impl for arbitrary widths is only co-simulated at small widths, which is a correctness gap rather than an equation-level circular step. Self-citations are not load-bearing here; the cited prior work is external and the Lean kernel provides independent checking. Overall, the main reduction is the specification-validation loop, warranting a score of 6.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

No fitted numerical parameters appear in the central claims; the reported numbers are evaluation metrics. The load-bearing assumptions are semantic faithfulness of the translator and of the LLM formalization, neither of which is proved for all parameter values.

axioms (4)
  • standard math Lean 4 kernel is sound
    The framework treats Lean's kernel and Mathlib as trusted; all proof claims inherit their soundness.
  • domain assumption Chisel-to-Lean translation preserves execution semantics for all parameters
    Phase I validates only small-bit-width co-simulation; no proof of semantic preservation for arbitrary parameter values is given.
  • domain assumption LLM formalization faithfully captures the natural-language specification
    Step 1 has the agent interpret NL requirements, and validation is done by co-simulation against the implementation, not by an independent specification oracle.
  • ad hoc to paper Small-bit-width co-simulation is representative of all widths
    The paper relies on exhaustive small-width co-simulation as 'additional confidence' rather than a proof, so width-dependent bugs would escape detection.

pith-pipeline@v1.3.0-daily-deepseek · 11415 in / 10275 out tokens · 98780 ms · 2026-08-01T15:47:11.316868+00:00 · methodology

0 comments
read the original abstract

Modern integrated circuits (ICs) are becoming increasingly complex, making functional verification a major bottleneck. The dominant hardware formal verification methodology, model checking, verifies each design instance separately and exposes only pass/fail results, so the reasoning behind a proof stays locked inside solver heuristics and is repeatedly reconstructed across related designs. Interactive theorem proving instead yields explicit, reusable proof artifacts, but applying it to hardware remains largely manual, demanding expert effort for formalization, invariant discovery, and proof development. In this paper, we present CircuitProver, an agentic Lean 4-based verification framework supporting proof-accumulation and parameterized verification. CircuitProver automatically translates parameterized hardware designs and their natural language specifications into executable Lean 4 models. It then iteratively constructs machine-checked proofs through Lean feedback to establish that the hardware code complies with the specification. The proving traces and verified theorems are distilled into reusable libraries, where proving strategies guide future agent reasoning and verified lemmas support formal proof reuse across related hardware verification tasks. We further introduce the first benchmark suite for evaluating agentic hardware theorem proving, covering diverse parameterized hardware designs, specifications, proof tasks, and evaluation metrics. Across 63 tasks, CircuitProver successfully proves all benchmarks, while a vanilla agent solves 92.1% of them and requires twice as many proof rounds on average. Ablation studies show that accumulated proof knowledge reduces redundant proof construction across related verification tasks, reducing proof length by 16.3% and verification time by 23.2%.

Figures

Figures reproduced from arXiv: 2607.27259 by Chen Chen, Hongce Zhang, Wenji Fang, Zhiyao Xie, Ziyi Yang.

Figure 1
Figure 1. Figure 1: Comparison between existing model checking and [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Workflow of CircuitProver for agentic hardware theorem proving. The framework translates hardware designs into [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Proof knowledge accumulation in CircuitProver. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Detailed proof strategy for the carry-skip adder [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Ablation study of CircuitProver, evaluating the im [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

50 extracted references · 11 linked inside Pith

  1. [1]

    Proceedings of the 49th annual design automation conference , pages=

    Chisel: constructing hardware in a scala embedded language , author=. Proceedings of the 49th annual design automation conference , pages=

  2. [2]

    International Conference on Automated Deduction , pages=

    The lean 4 theorem prover and programming language , author=. International Conference on Automated Deduction , pages=. 2021 , organization=

    2021

  3. [3]

    Communications of the ACM , volume=

    Formal verification of a realistic compiler , author=. Communications of the ACM , volume=. 2009 , publisher=

    2009

  4. [4]

    Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon , booktitle=

  5. [5]

    Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages=

    The. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages=

  6. [6]

    Replacing testing with formal verification in

    Kaivola, Roope and Ghughal, Rajnish and Narasimhan, Naren and Telfer, Amber and Whittemore, Jesse and Pandav, Sudhindra and Slobodova, Anna and Taylor, Christopher and Frolov, Vladimir and Reeber, Erik and Naik, Armaghan , booktitle=. Replacing testing with formal verification in. 2009 , organization=

    2009

  7. [7]

    Yao, Shunyu and Zhao, Jeffrey and Yu, Dian and Du, Nan and Shafran, Izhak and Narasimhan, Karthik and Cao, Yuan , booktitle=

  8. [8]

    Advances in Neural Information Processing Systems , year=

    Reflexion: Language Agents with Verbal Reinforcement Learning , author=. Advances in Neural Information Processing Systems , year=

  9. [9]

    and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , booktitle=

    Yang, Kaiyu and Swope, Aidan M. and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima , booktitle=

  10. [10]

    Wang, Keyin and Shi, Xiaomu and Liu, Jiaxiang and Wu, Zhilin and Chen, Taolue and Song, Fu and Jansen, David N. , year=. A Formally Verified Procedure for Width Inference in. 2601.12813 , archivePrefix=

    arXiv

  11. [11]

    Proceedings of the ACM on Programming Languages , volume=

    Kami: a platform for high-level parametric hardware specification and its modular verification , author=. Proceedings of the ACM on Programming Languages , volume=. 2017 , publisher=

    2017

  12. [12]

    Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences , volume=

    Industrial hardware and software verification with ACL2 , author=. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences , volume=. 2017 , publisher=

    2017

  13. [13]

    Proceedings of the 61st ACM/IEEE Design Automation Conference , pages=

    Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once , author=. Proceedings of the 61st ACM/IEEE Design Automation Conference , pages=

  14. [14]

    Communications of the ACM , volume=

    Model checking: algorithmic verification and debugging , author=. Communications of the ACM , volume=. 2009 , publisher=

    2009

  15. [15]

    2011 Formal Methods in Computer-Aided Design (FMCAD) , pages=

    Efficient implementation of property directed reachability , author=. 2011 Formal Methods in Computer-Aided Design (FMCAD) , pages=. 2011 , organization=

    2011

  16. [16]

    , author=

    Bounded model checking. , author=. Handbook of satisfiability , volume=

  17. [17]

    International Conference on Computer Aided Verification , pages=

    Pono: a flexible and extensible SMT-based model checker , author=. International Conference on Computer Aided Verification , pages=. 2021 , organization=

    2021

  18. [18]

    IEEE Transactions on Software Engineering , volume=

    An industrial strength theorem prover for a logic based on Common Lisp , author=. IEEE Transactions on Software Engineering , volume=. 1997 , publisher=

    1997

  19. [19]

    International Conference on Certified Programs and Proofs , pages=

    Coquet: a coq library for verifying hardware , author=. International Conference on Certified Programs and Proofs , pages=. 2011 , organization=

    2011

  20. [20]

    VLSI specification, verification and synthesis , pages=

    HOL: A proof generating system for higher-order logic , author=. VLSI specification, verification and synthesis , pages=. 1988 , publisher=

    1988

  21. [21]

    arXiv preprint arXiv:2605.07782 , year=

    CktFormalizer: Autoformalization of Natural Language into Circuit Representations , author=. arXiv preprint arXiv:2605.07782 , year=

    Pith/arXiv arXiv

  22. [22]

    arXiv preprint arXiv:2405.14333 , year=

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data , author=. arXiv preprint arXiv:2405.14333 , year=

    Pith/arXiv arXiv

  23. [23]

    arXiv preprint arXiv:2310.10631 , year=

    Llemma: An open language model for mathematics , author=. arXiv preprint arXiv:2310.10631 , year=

    Pith/arXiv arXiv

  24. [24]

    arXiv preprint arXiv:2210.12283 , year=

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs , author=. arXiv preprint arXiv:2210.12283 , year=

    Pith/arXiv arXiv

  25. [25]

    arXiv preprint arXiv:2109.00110 , year=

    Minif2f: a cross-system benchmark for formal olympiad-level mathematics , author=. arXiv preprint arXiv:2109.00110 , year=

    Pith/arXiv arXiv

  26. [26]

    arXiv preprint arXiv:2302.12433 , year=

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics , author=. arXiv preprint arXiv:2302.12433 , year=

    Pith/arXiv arXiv

  27. [27]

    arXiv preprint arXiv:2607.09217 , year=

    OpenProver: Agentic and Interactive Theorem Proving with Lean 4 , author=. arXiv preprint arXiv:2607.09217 , year=

    Pith/arXiv arXiv

  28. [28]

    International Conference on Intelligent Computer Mathematics , pages=

    Growing Mathlib: maintenance of a large scale mathematical library , author=. International Conference on Intelligent Computer Mathematics , pages=. 2025 , organization=

    2025

  29. [29]

    International Conference on Learning Representations , volume=

    Automated proof generation for rust code via self-evolution , author=. International Conference on Learning Representations , volume=

  30. [30]

    Proceedings of the ACM on Programming Languages , volume=

    Aeneas: Rust verification by functional translation , author=. Proceedings of the ACM on Programming Languages , volume=. 2022 , publisher=

    2022

  31. [31]

    The AIGER And-Inverter Graph (AIG) Format Version , volume=

    The aiger and-inverter graph (aig) format version 20070427 , author=. The AIGER And-Inverter Graph (AIG) Format Version , volume=

  32. [32]

    International Conference on Computer Aided Verification , pages=

    Btor2, btormc and boolector 3.0 , author=. International Conference on Computer Aided Verification , pages=. 2018 , organization=

    2018

  33. [33]

    Language c , pages=

    The smt-libv2 language and tools: A tutorial , author=. Language c , pages=

  34. [34]

    Proceedings of the 30th Asia and South Pacific Design Automation Conference , pages=

    Assertllm: Generating hardware verification assertions from design specifications via multi-llms , author=. Proceedings of the 30th Asia and South Pacific Design Automation Conference , pages=

  35. [35]

    arXiv preprint arXiv:2510.15906 , year=

    FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures , author=. arXiv preprint arXiv:2510.15906 , year=

    arXiv

  36. [36]

    arXiv preprint arXiv:2511.17833 , year=

    Learning to Debug: LLM-Organized Knowledge Trees for Solving RTL Assertion Failures , author=. arXiv preprint arXiv:2511.17833 , year=

    arXiv

  37. [37]

    Findings of the Association for Computational Linguistics: NAACL 2025 , pages=

    Assertionbench: A benchmark to evaluate large-language models for assertion generation , author=. Findings of the Association for Computational Linguistics: NAACL 2025 , pages=

    2025

  38. [38]

    The lean mathematical library , booktitle=

    The mathlib Community , year=. The lean mathematical library , booktitle=

  39. [39]

    International Conference on Learning Representations , volume=

    Lego-prover: Neural theorem proving with growing libraries , author=. International Conference on Learning Representations , volume=

  40. [40]

    International Conference on Learning Representations , volume=

    Leanagent: Lifelong learning for formal theorem proving , author=. International Conference on Learning Representations , volume=

  41. [41]

    Advances in neural information processing systems , volume=

    Autoformalization with large language models , author=. Advances in neural information processing systems , volume=

  42. [42]

    arXiv preprint arXiv:2404.12534 , year=

    Towards large language models as copilots for theorem proving in lean , author=. arXiv preprint arXiv:2404.12534 , year=

    Pith/arXiv arXiv

  43. [43]

    IEEE Micro , year=

    XiangShan: An open-source project for high-performance RISC-V processors meeting industrial-grade standards , author=. IEEE Micro , year=

  44. [44]

    2016 , publisher=

    The rocket chip generator , author=. 2016 , publisher=

    2016

  45. [45]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , volume=

    r-map: Relating implementation and specification in hardware refinement checking , author=. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , volume=. 2023 , publisher=

    2023

  46. [46]

    arXiv preprint arXiv:2606.28279 , year=

    Agentic Hardware Design as Repository-Level Code Evolution , author=. arXiv preprint arXiv:2606.28279 , year=

    Pith/arXiv arXiv

  47. [47]

    RTL: Autonomous Agentic RTL Optimization through Tool-Grounded Self-Improvement , author=

    Dr. RTL: Autonomous Agentic RTL Optimization through Tool-Grounded Self-Improvement , author=. arXiv preprint arXiv:2604.14989 , year=

    Pith/arXiv arXiv

  48. [48]

    Advances in Neural Information Processing Systems , volume=

    Apollo: Automated llm and lean collaboration for advanced formal reasoning , author=. Advances in Neural Information Processing Systems , volume=

  49. [49]

    arXiv preprint arXiv:2412.20735 , year=

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving , author=. arXiv preprint arXiv:2412.20735 , year=

    Pith/arXiv arXiv

  50. [50]

    FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping , year=

    Yang, Ziyi and Hu, Guangyu and Zhou, Xiaofeng and Miao, Mingkai and Yu, Changyuan and Zhang, Wei and Zhang, Hongce , booktitle=. FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping , year=