# Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning

arXiv: https://arxiv.org/abs/2509.06239 · HTML: https://mlsanity.com/paper/2509.06239/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in RL training of language and agent models, one of 15 directions in Deep reinforcement learning methods.
- Builds on 20 of its 29 references that are in the map.
- First posted on arXiv 7 Sep 2025.

## Placed in

- Deep reinforcement learning methods / [RL training of language and agent models](https://mlsanity.com/deeprl/rl-training-of-language-and-agent-models/)

## Builds on (most cited first, 20 of 20)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [Guiding Pretraining in Reinforcement Learning with Large Language Models](https://mlsanity.com/paper/2302.06692/) (2023)
- [Evaluation of OpenAI o1: Opportunities and Challenges of AGI](https://mlsanity.com/paper/2409.18486/) (2024)
- [Learning Dynamics of LLM Finetuning](https://mlsanity.com/paper/2407.10490/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [HLSPilot: LLM-based High-Level Synthesis](https://mlsanity.com/paper/2408.06810/) (2024)
- [ScaleHLS: A New Scalable High-Level Synthesis Framework on Multi-Level Intermediate Representation](https://mlsanity.com/paper/2107.11673/) (2021)
- [CreativEval: Evaluating Creativity of LLM-Based Hardware Code Generation](https://mlsanity.com/paper/2404.08806/) (2024)
- [Spec2RTL-Agent: Automated Hardware Code Generation from Complex Specifications Using LLM Agent Systems](https://mlsanity.com/paper/2506.13905/) (2025)
- [VerilogReader: LLM-Aided Hardware Test Generation](https://mlsanity.com/paper/2406.04373/) (2024)
- [YOLO-MARL: You Only LLM Once for Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2410.03997/) (2024)
- [LERO: LLM-driven Evolutionary framework with Hybrid Rewards and Enhanced Observation for Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2503.21807/) (2025)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis](https://mlsanity.com/paper/2410.19736/) (2024)
- [Dafny as Verification-Aware Intermediate Language for Code Generation](https://mlsanity.com/paper/2501.06283/) (2025)

## Built on by (most cited first, 1 of 1)

- [A Survey of Reinforcement Learning for Large Reasoning Models](https://mlsanity.com/paper/2509.08827/) (2025)

## Abstract (arXiv)

Large Language Models (LLMs) have demonstrated impressive capabilities in automated code generation but frequently produce code that fails formal verification, an essential requirement for hardware and safety-critical domains. To overcome this fundamental limitation, we previously proposed PREFACE, a model-agnostic framework based on reinforcement learning (RL) that iteratively repairs the prompts provided to frozen LLMs, systematically steering them toward generating formally verifiable Dafny code without costly fine-tuning. This work presents Proof2Silicon, a novel end-to-end synthesis framework that embeds the previously proposed PREFACE flow to enable the generation of correctness-by-construction hardware directly from natural language specifications. Proof2Silicon operates by: (1) leveraging PREFACE's verifier-driven RL agent to optimize prompt generation iteratively, ensuring Dafny code correctness; (2) automatically translating verified Dafny programs into synthesizable high-level C using Dafny's Python backend and PyLog; and (3) employing Vivado HLS to produce RTL implementations. Evaluated rigorously on a challenging 100-task benchmark, PREFACE's RL-guided prompt optimization consistently improved Dafny verification success rates across diverse LLMs by up to 21%. Crucially, Proof2Silicon achieved an end-to-end hardware synthesis success rate of up to 72%, generating RTL designs through Vivado HLS synthesis flows. These results demonstrate a robust, scalable, and automated pipeline for LLM-driven, formally verified hardware synthesis, bridging natural-language specification and silicon realization.