WybeCoder: Verified Imperative Code Generation
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915937595162624 |
|---|---|
| author | Gloeckle, Fabian Baksys, Mantas Feher, Darius Zheng, Kunhao Hayat, Amaury Holden, Sean B. Synnaeve, Gabriel O'Hearn, Peter |
| author_facet | Gloeckle, Fabian Baksys, Mantas Feher, Darius Zheng, Kunhao Hayat, Amaury Holden, Sean B. Synnaeve, Gabriel O'Hearn, Peter |
| contents | Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development, in which code, invariants, and proofs co-evolve. WybeCoder builds on a recent framework that combines automatic verification condition generation and SMT solving with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, into equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements as we scale our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, ultimately producing hundreds of lines of verified code and overcoming plateaus reported in previous work. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, substantially surpassing previous evaluations and paving the way for the automated construction of large-scale datasets of verified imperative code. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_29088 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | WybeCoder: Verified Imperative Code Generation Gloeckle, Fabian Baksys, Mantas Feher, Darius Zheng, Kunhao Hayat, Amaury Holden, Sean B. Synnaeve, Gabriel O'Hearn, Peter Software Engineering Artificial Intelligence Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development, in which code, invariants, and proofs co-evolve. WybeCoder builds on a recent framework that combines automatic verification condition generation and SMT solving with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, into equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements as we scale our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, ultimately producing hundreds of lines of verified code and overcoming plateaus reported in previous work. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, substantially surpassing previous evaluations and paving the way for the automated construction of large-scale datasets of verified imperative code. |
| title | WybeCoder: Verified Imperative Code Generation |
| topic | Software Engineering Artificial Intelligence |
| url | https://arxiv.org/abs/2603.29088 |