Search papers, labs, and topics across Lattice.
WybeCoder is introduced as an agentic code verification framework that integrates automatic verification condition generation, SMT solvers, and interactive proofs in Lean to enable prove-as-you-generate development. The framework was evaluated by translating functional verification benchmarks (Verina and Clever) into imperative code specifications. Results show that WybeCoder significantly improves performance on complex algorithms like Heapsort, achieving 74% and 62% solve rates on Verina and Clever, respectively, outperforming prior work and suggesting a path towards large-scale verified code datasets.
LLMs can now automatically verify imperative code during generation, achieving state-of-the-art results on complex algorithms and opening the door to large-scale datasets of verified code.
Recent progress in large language models (LLMs) has advanced automatic code generation and formal theorem proving, yet software verification has not seen the same improvement. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development where code, invariants, and proofs co-evolve. It builds on a recent framework that combines automatic verification condition generation and SMT solvers with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, to equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements by scaling our approach, synthesizing dozens of valid invariants and dispatching of dozens of subgoals, resulting in hundreds of lines of verified code, overcoming plateaus reported in previous works. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, significantly surpassing previous evaluations and paving a path to automated construction of large-scale datasets of verified imperative code.
