AI RESEARCH

VERINA: Benchmarking Verifiable Code Generation

arXiv CS.AI

ArXi:2505.23135v3 Announce Type: replace-cross Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding.