Preprint

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability

Shirley Yu Ruben Martins

Jul 2026 · 0 citations · 29 references

Computer Science

TL;DR

It is shown that task-equivalent implementations can differ substantially in verifiability and that implementation diversity helps find verification-friendly artifacts, and that implementation diversity helps find verification-friendly artifacts.

Abstract

Program verification is crucial for software correctness, but producing fully verified programs remains difficult in practice. This paper studies whether implementation structure affects automated verifiability when multiple generated programs are intended to satisfy the same task-level semantics. We present Diversify2Verify, a staged LLM-based pipeline for Why3 that infers representation-specific contracts, generates and tests diverse recursive and imperative array/list implementations, and attempts verification with bounded verifier-guided annotation repair. We also construct a verification-oriented benchmark of 73 tasks over integers, arrays, and lists, yielding 292 implementation variants. Diversify2Verify verifies 96 artifacts initially and 154 after two repair passes, improving artifact-level verification from 32.9% to 52.7%. At the task level, at least one variant verifies for 49 of 73 tasks, a 67.1% success rate. These results show that task-equivalent implementations can differ substantially in verifiability and that implementation diversity helps find verification-friendly artifacts.

arXiv Semantic Scholar

View source

Similar papers

Preprint Aug 2026

How Powerful are LLMs in Generating Formal Program Specifications?

Coins is introduced, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations, and finds that accurate specification evaluation, rather than model scaling alone, is central to understanding the...

Fan-Peng Yang, Xing Li, Shu-Ling Wang et al. · 0 citations

Jul 2026

BTOR2-Based C Program Verification via Hardware Model Checking

C2Btor, a method for encoding verification tasks into BTOR2 models that allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.

Xinyu Zhang, Runxuan Fang, Ziqun Bao et al. · arXiv.org · 0 citations

Jul 2026

Foundational Constraint Solving for Expressive Refinement Typing

FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.

J. Khan, Petros Markopoulos, Nicolás Lehmann et al. · arXiv.org · 0 citations

Preprint Aug 2026

Security Tests as Executable Specifications for LLM Code Generation: Benefits, Trade-offs, and Coverage Limits

The results show that executable feedback can repair secure-code generation, but its benefits depend on the model, task, feedback entry point, and especially test coverage.

Yun-Hao Liang, Cheng-Guang Gan, Rui-Xuan Ying et al. · 2 citations

Preprint Aug 2026

GateTruth: Auditing the Rigor of RTL Design Benchmarks via Mutation Testing

GateTruth, a mutation-testing engine and methodology for auditing RTL benchmark testbench rigor, is introduced and it is argued mutation-kill certification should become a standard reporting requirement for RTL-generation benchmarks generally.

Meet Bhadra · 1 citation

Review Aug 2026

Combining Tests and Proofs with Contracts for Better Software Verification

Three applications, leveraging on the mechanisms of Eiffel and design by contract, hold significant promise to address some of the challenges of program testing, software maintenance, and automatic program repair.

Li Huang, Bertrand Meyer, M. Oriol · Communications of the ACM · 0 citations