Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.23241

Towards Agentic Proof Harness Engineering

Rohith Kumar Shanmuganathan·Cedric Richter·Heike Wehrheim
View original source ↗Read source document ↗Export metadata ↓

Abstract

Formal verification of real-world projects requires substantial manual effort, from specifying correctness properties to constructing the infrastructure needed to check them. We envision verification agents that assist developers throughout this process. Among the many tasks involved, one stands out as both foundational and amenable to automation: proof-harness engineering. A proof harness defines an isolated verification environment for a program unit, such as a function or module, by providing symbolic inputs, initialization code, and models of its dependencies. Today, proof-harness engineering remains largely a manual task performed by verification engineers. To explore the potential of coding agents for this task, we propose an agentic proof-harness engineer that automatically constructs verifier-ready harnesses from a software project and a designated verification target. We combine the agent with formal soundness and precision guards to validate generated abstractions and guide their refinement. We evaluate the feasibility of our approach in an exploratory case study on curl and libuv, using three historical assertion violations already embedded in the source code as verification properties. Our results show that the agent successfully constructs proof harnesses that enable CBMC to detect all three violations. We further demonstrate the potential for reusing these harnesses with other verification tools.

Explore related subjects

cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Rohith Kumar Shanmuganathan, Cedric Richter, Heike Wehrheim. 2026-10-16. Towards Agentic Proof Harness Engineering. https://arxiv.org/abs/2610.23241

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Pluvio: Assembly Clone Search for Out-of-domain Architectures and Libraries through Transfer Learning and Conditional Variational Information Bottleneck

The practice of code reuse is crucial in software development for a faster and more efficient development lifecycle. In reality, however, code reuse practices lack proper control, resulting in issues such as vulnerability propagation and intellectual property infringements. Assembly clone search, a critical shift-right defence mechanism, has been effective in identifying vulnerable code resulting from reuse in released executables. Recent studies on assembly clone search demonstrate a trend towards using machine learning-based methods to match assembly code variants produced by different toolchains. However, these methods are limited to what they learn from a small number of toolchain variants used in training, rendering them inapplicable to unseen architectures and their corresponding compilation toolchain variants. This paper presents the first study on the problem of assembly clone search with unseen architectures and libraries. We propose incorporating human common knowledge through large-scale pre-trained natural language models, in the form of transfer learning, into current learning-based approaches for assembly clone search. Transfer learning can aid in addressing the limitations of the existing approaches, as it can bring in broader knowledge from human experts in assembly code. We further address the sequence limit issue by proposing a reinforcement learning agent to remove unnecessary and redundant tokens. Coupled with a new Variational Information Bottleneck learning strategy, the proposed system minimizes the reliance on potential indicators of architectures and optimization settings, for a better generalization of unseen architectures. We simulate the unseen architecture clone search scenarios and the experimental results show the effectiveness of the proposed approach against the state-of-the-art solutions.

cs.SE↗
arXiv2026

FeatureFuzz: Treating Bug-prone Features as Core Primitives for Compiler Fuzzing

CI/CD pipelines often execute build and test tasks with high privileges, making the compilation stage security-sensitive. In this setting, malicious pull requests may exploit carefully crafted source code to trigger arbitrary code execution or excessive resource consumption during compilation, making compiler vulnerabilities security-relevant. Recent work has leveraged bug-prone knowledge from historical bugs to drive compiler exploration and bug discovery. However, many compiler bugs depend on program semantics rather than syntax, and existing approaches either rely on syntactic mutation or encode this knowledge in model parameters, making it difficult to preserve and recombine the semantics that actually trigger compiler bugs. We propose FeatureFuzz, a compiler fuzzer that explicitly reuses bug-prone semantics through features and feature groups. FeatureFuzz extracts these bug-prone semantics from historical bugs as features, synthesizes them into coherent feature groups, and instantiates them into programs for compiler fuzzing. On GCC and LLVM, over 24-hour campaigns, FeatureFuzz uncovers 167 unique crashes, 2.78x as many as the second-best fuzzer. Over a 72-hour fuzzing campaign, FeatureFuzz identifies 122 bugs, of which 106 have been confirmed by compiler developers as zero-days. Among reported bugs, 64 affect release-build compilers, including 9 memory-corruption bugs, highlighting the security relevance of compiler fuzzing in CI/CD settings.

cs.SE↗
arXiv2026

A Theoretical Analysis of Test-Driven Code Generation

Code assistants are increasingly utilized in test-driven software development, yet the theoretical mechanisms behind their environment-interaction strategies remain underexplored. We provide a probabilistic framework for two dominant paradigms: code selection after generation using the execution environment, and code generation conditioned on environment feedback. First, we formalize several well-established selection heuristics as environment-aware estimators of code correctness. We theoretically prove that estimators based on fuzzy functional similarity add an inductive bias and strictly dominate estimators based on functional equivalence in terms of signal-to-noise ratio. Second, we frame backprompting as an in-context approximation of Thompson sampling. We derive a novel regret bound for reward functions with unobservable components, theoretically explaining why the effectiveness of backprompting is limited by the ambiguity of the informal task description (an irreducible regret). Using seven state-of-the-art open weight models, we corroborate these findings across BigCodeBenchHard, LeetCodeDataset, QiskitHumanEvalSim, and SWE-bench Verified. Our formalization also suggests how to improve task descriptions effectively, leading to an improved benchmark for LLM-assisted quantum programming, QiskitHumanEvalSimX.

cs.SE↗