Diffusion Models for Code Verification

Large language models have made generating code much easier, but checking that the code is correct remains difficult. Formal verification addresses this gap with a specification and a machine-checked proof, yet finding that proof can require many rounds of generation and repair. We explore diffusion and self-speculative decoding as alternatives to autoregressive generation for code verification in Lean. Diffusion can generate tokens in parallel and use bidirectional context to fill missing code and proof regions; self-speculation combines parallel drafting with causal checking. We train one 8B hybrid model on 600,000 decomposition, completion, and repair transitions, and use the same weights for all three decoding modes. Local repair revises an individual proof body, while global refinement revises related proof bodies together after repeated local failure. The goal is to finish a program and a proof that Lean accepts. Across VERINA and CLEVER, our strongest configuration with global refinement verifies up to $1.4\times$ as many tasks as the Goedel-Code-Prover baseline under the same search limits. Both diffusion and self-speculation use parallel generation and surrounding proof context to support faster completion and repair. We release our training data, checkpoints, and codebase so the community can build on this work.