Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
- URL: http://arxiv.org/abs/2608.29716v1
- Date: Sun, 30 Aug 2026 10:50:56 GMT
- Title: Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
- Abstract summary: We report on the verification of memory safety for decoder components of liblzma.<n>The verification exposed undefined behavior in raw LZMA1 zero-input handling.<n>Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C.
- Score: 32.505127447635864
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it controls, the outer decoding path, and the shared sliding-window dictionary. Built with the Verified Software Toolchain (VST), machine-checked body theorems establish memory safety and partial functional correctness. Across 27 completed body proofs, the largest covers lzma decode, whose 338 source lines expand to 1,934 lines of C after preprocessing; its proof comprises 183,268 lines of proof script over 775,768 lines of mechanically extracted goal statements. The verification exposed undefined behavior in raw LZMA1 zero-input handling, where range-decoder macros add zero to a null pointer and subtract two null pointers. Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C. AI agents complete proof goals and propose refinements; humans write and review models and specifications, and approve semantic changes; the Rocq kernel checks the proof terms. With agents constructing the proof scripts, the main engineering problems lay in translating and modeling production C, building a robust harness for driving Rocq, and providing feedback for proving agents. VST's assertion logic expressed every contract required by the development. We describe the pipeline, coordination mechanisms, and proof-engineering techniques that resolved these frictions.
Related papers
- Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
arXiv Detail & Related papers (2026-08-13T17:41:27Z) - An AI Approach to Verified Production Cryptographic Libraries [5.564288012051712]
We present CryptoProver, an AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts.<n>Without changing executable code, CryptoProver constructs a new independent proof of curve25519-dalek.
arXiv Detail & Related papers (2026-08-02T03:32:08Z) - The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
In a verifier-driven loop, AI agents wrote and verified bare-metal security software in Ada/SPARK spanning classical and post-quantum cryptography, TLS 1.3, IKEv2, X.509, and a Matrix client.<n>GNATprove discharged 49,280 proof obligations, established functional correctness for selected primitives, and proved the absence of run-time errors for the rest.<n>We report where each layer caught faults and draw the central lesson: what an agent can be trusted to establish is bounded by the strength of its feedback.
arXiv Detail & Related papers (2026-07-15T20:09:05Z) - From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
Productization adds requirements for source boundaries, entity routing, answer contracts, and reproducible traces.<n>We present a harness-engineering approach that reconstructs this pattern into a traceable, auditable LLM-agent architecture.<n>We instantiate it on a public-data slice of five Korean corporate groups and evaluate three research questions.
arXiv Detail & Related papers (2026-07-09T01:08:33Z) - Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
This submission includes a complete reference implementation together with deterministic test vectors and a reproducible benchmark suite.<n>The AEAD construction is fully specified, including domain separation, rate and capacity choices, tag generation, and the exact file format used by the reference CLI.<n>Reported performance numbers are produced by the built in benchmark tool under documented hardware and compiler settings.
arXiv Detail & Related papers (2026-02-19T23:39:54Z) - Verifiable Provenance of Software Artifacts with Zero-Knowledge Compilation [5.939983212292006]
We propose a novel approach to verifiable provenance based on compiling software with zero-knowledge virtual machines (zkVMs)<n>By executing a compiler within a zkVM, our system produces both the compiled output and a cryptographic proof attesting that the compilation was performed on the claimed source code with the claimed compiler.<n>Our results show that zk-compilation is applicable to real-world software and provides strong security guarantees.
arXiv Detail & Related papers (2026-02-12T12:36:36Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
arXiv Detail & Related papers (2026-01-30T08:29:01Z) - Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
arXiv Detail & Related papers (2025-06-24T13:42:59Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
arXiv Detail & Related papers (2025-05-28T17:57:47Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
arXiv Detail & Related papers (2024-10-21T08:15:45Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.