PaperlayerView exact revision on arXiv

Source-linked AI summary

Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST

Prokhor Shlyakhtun, Alexander Gryzlov, Vladimir Kukharenko, Vasilii Nesterov, Nikolai Vasiliev, Kirill Ziborov, Eugene Zolotarev, Alex Pokras

arXiv:2608.29716v1cs.SE

TL;DR

The paper addresses whether production-scale liblzma decoder components can be verified for memory safety under explicit contracts. It combines VST body proofs with an agent–human workflow, closing decoder theorems and exposing undefined behavior in raw LZMA1 zero-input handling. The results establish contract-relative Clight safety and partial functional correctness for the verified scope, while the reported scale reflects development effort rather than a human-only savings comparison.

  • Problem

    The paper asks whether pre-existing, production-scale liblzma decoder bodies can be proved safe under explicit function contracts.

  • Method

    The workflow assigns proof construction and repair to AI agents, keeps model and specification authority with humans, and uses VST with Rocq kernel checking for decoder body proofs.

  • Results

    22 closed VST body theorems establish Clight safety and model-relative partial functional correctness for the listed decoder components, while verification exposes undefined behavior in raw LZMA1 zero-input handling.

  • Takeaways & Limitations

    The development demonstrates that contract-relative memory-safety verification can be applied to selected production liblzma decoder components using an agent–human proof workflow.

  • Takeaways & Limitations

    The reported figures characterize scale and observed outcomes, not human effort or labor savings, because no human-only baseline is available.

Abstract

from arXiv · show

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.

1 Introduction

The paper verifies pre-existing liblzma decoder code with an agent–human workflow in which agents construct proofs while humans control models and specifications. The development closes body proofs for key decoder components, scales to large production C, and exposes undefined behavior in raw LZMA1 zero-input handling.

  • The study asks whether liblzma decoder bodies can be proved safe under explicit function contracts.
  • Agents construct and repair VST proofs, while humans approve every model or function-specification change before dependent proofs are updated.The Rocq kernel checks the resulting proof terms.
  • 22 closed VST body proofs cover the LZMA2 state machine, outer decoding path, sliding-window dictionary, supporting LZMA1 functions, and LZMA1 decoding core.Each theorem establishes Clight safety and model-relative partial functional correctness under its precondition and imported contracts.
  • 183,268 lines of proof script verify lzma decode, whose 338-line function expands to 1,934 nonblank C lines after preprocessing.The verified function replaces the original Duff’s-device control flow with an explicit state machine.
  • Verification exposed undefined behavior in raw LZMA1 zero-input handling, where range-decoder macros perform invalid pointer arithmetic on null pointers.
  • Agent-driven proof development required Rocq interaction, goal extraction, orchestration, durable handoffs, build-aware C generation, model testing, and source normalization.

2 Background

The background defines VST body theorems as contract-relative guarantees over CompCert’s Clight semantics and situates them in liblzma’s range-coded, sliding-window decoder. The verified scope covers selected decoder components while excluding container parsing, filters, metadata, and encoders.

  • The Verified Software Toolchain: VST uses separation-logic ownership, disjoint P∗Q footprints, and framing to support modular reasoning about pointer-rich decoder structures.
  • The Verified Software Toolchain: Verifiable C translates preprocessed C into CompCert’s Clight representation, while funspecs specify logical parameters, owned memory, return values, and updated memory.Assertions such as data at and field at connect logical values to C objects and fields.
  • The Verified Software Toolchain: VST proof scripts use forward symbolic-execution tactics and entailment automation, with the Rocq kernel checking the assembled proof term.
  • The Verified Software Toolchain: A closed semax body theorem proves a function body cannot get stuck in Clight and, on normal return, satisfies its model-derived postcondition.The guarantee assumes the function’s funspec precondition and imported contracts, and includes memory faults represented as stuck execution.
  • The liblzma Library: Figure 1 identifies control flow, byte flow, suspension and resumption loops, and the enclosed verified portion of the LZMA2 decoding path.
  • The liblzma Library: liblzma interleaves adaptive binary range coding with an LZ77-style dictionary whose fixed-size circular buffer supports overlapping match copies.
  • The liblzma Library: The verified scope spans LZMA2 framing, the outer decoding path, the shared sliding-window dictionary, six supporting LZMA1 functions, and the structured LZMA1 core.It excludes the .xz container and integrity layer, filter framework, index and metadata machinery, and all encoders.
  • The liblzma Library: Figure 2 presents the model–specification–proof workflow and the C-to-Clight ingestion path used for build-aware verification.

3 The Agent-Driven Pipeline

The pipeline combines build-aware modeling, agent-driven proof construction, and human control over semantic artifacts. It scales large VST proofs by extracting goals, coordinating specialized agents, and optimizing proof-checking performance.

  • 3.1 Workflow: Model and Spec stages define executable abstract state transitions and VST predicates relating those states to C structs and buffers.The model preserves coupled range-decoding and symbol-interpretation state across resumable calls.
  • 3.1 Workflow: Humans retain authority over models and function specifications, while agents construct, repair, and propagate body proofs.Contract fixes are reported for human review rather than applied autonomously.
  • 3.2 Coordinating Large Proofs: Goal extraction converts live mid-proof subgoals into standalone definitions and lemma skeletons, enabling parallel work without refactoring VST semax proofs.The extracted hypotheses are lifted under universal quantifiers to make each goal self-contained.
  • 3.2 Coordinating Large Proofs: Proving subagents are restricted to assigned proof files and may add helper lemmas but cannot change definitions, theorem statements, or funspecs.An orchestrator compiles completed files and routes contract changes through a separate human-reviewed repair path.
  • 3.2 Coordinating Large Proofs: Mechanical hooks block autogenerated-goal inspection and cold coqc checks while flagging proof-checking timeouts as proof problems.These guardrails keep agents on the incremental rocq-lsp workflow and discourage routing around difficult goals.
  • 3.3 Proof Optimization: Most optimized proof files became at least 30% faster to check in wall-clock time.Agents profiled files, refactored recurring bottlenecks, and scheduled follow-up optimization tasks.

4 A Reviewed Coupling Invariant

The reviewed invariant couples each LZMA2 framing phase to the initialization stage of its embedded LZMA1 child. An agent-detected unreachable state led to a human-approved strengthening propagated through all affected proof sites.

  • 4 A Reviewed Coupling Invariant: The invariant relates outer LZMA2 phases to four embedded-child stages: NoChild, Raw, Sized, and DecodeReady.These stages distinguish installation, output-size assignment, and readiness after reset.
  • 4 A Reviewed Coupling Invariant: Raw children cannot be in Properties or Lzma, preventing an allocated child from being used as initialized.Once properties are available, the next header phase must be Properties.
  • 4 A Reviewed Coupling Invariant: Sized children cannot enter Lzma or Copy before reset makes them ready to decode.This excludes transitions during the interval after output-size assignment and before reset.
  • 4 A Reviewed Coupling Invariant: At Control, a child that is not DecodeReady still requires properties, while Lzma requires DecodeReady during normal progression.The invariant also constrains Copy and Properties transitions according to header and child stage.
  • 4 A Reviewed Coupling Invariant: An agent found that the original Copy alternative admitted the unreachable Sized/Copy state, so it reported a proposed invariant strengthening instead of changing the specification.The specification owner approved the change, after which agents re-established it at nine producer sites and its consumers.

5 Proof Engineering for Production C and VST

Making production liblzma C verifiable required build-aware translation, executable model validation, and source normalization for constructs outside Verifiable C. Differential execution exposed model discrepancies before formal body proofs.

  • 5.1 Pipeline: The C-to-proof path recovers build-configured source, tests the functional model against executions, and regularizes unsupported C constructs.These steps address translation fidelity, semantic validation, and Verifiable C compatibility.
  • 5.1 Pipeline: Build-aware extraction runs CMake with a compiler wrapper to recover the macros, include paths, and preprocessor flags selected for each translation unit.Generic preprocessing exposes expanded source but does not discover the build system’s configured definitions and include paths.
  • 5.2 Execution Grounding: Differential execution compares the functional model with configured C runs before expensive body proofs, including intermediate state across resumable decoder calls.LLDB snapshots are lifted into Rocq representations and compared with model outcomes through JSONL traces and vm compute.
  • 5.2 Execution Grounding: Six corrective Git commits fixed model discrepancies involving probability offsets, position state, literal and repetition tracking, range-coder threading, and stopping behavior.The tests localized mismatches before corresponding body-proof construction.
  • 5.3 C Standards Mismatches and Source Normalization: The proof retained xz’s index -1 probability-tree access using CompCert’s lower-level offset representation, despite ISO C defining such pointer arithmetic as undefined behavior.The source was left unchanged because CompCert permits forming out-of-bounds pointers when they are not unsafely dereferenced or compared.
  • 5.3 C Standards Mismatches and Source Normalization: Aggregate assignments were expanded fieldwise, goto-based state saving became a returning macro, and Duff’s device was replaced with structured state-machine dispatch.These changes made the source acceptable to Verifiable C without changing the intended behavior of the relevant operations.

6 Evaluation

The evaluation measures the verification’s scope, proof scale, exposed undefined behavior, and agentic development resources. The closed proofs establish safety only under stated preconditions and imported contracts, with important scope and accounting boundaries.

  • The verification evaluates a source-level defect, formal proof scope and scale, and resources used by the agentic workflow.
  • Undefined behavior: The raw LZMA1 zero-input path performs undefined pointer arithmetic by adding zero to a null pointer and subtracting two null pointers.The path is reached when raw decoding accepts a zero-input call after consuming its five-byte range-decoder prefix.
  • Verification scope: 22 closed body theorems cover decoder components, while the broader inventory contains 27 closed body theorems including five supporting common-layer bodies.The decoder scope excludes the container/stream layer, filter framework, and encoders.
  • Proof scale: 42% of the extracted-proof lines are repeated blocks, while symbolic-execution forward steps account for about 2%.The largest repeated argument is an 18-conjunct decoder-state well-formedness proof written 63 times.
  • Agentic development: Project records report 1,595 agent sessions and six corrective Git commits, but do not provide human-effort accounting or a human-only baseline.The missing accounting would require recovering and auditing unavailable interaction logs.
  • Scope and assumptions: The transformed verified-xz snapshot establishes Clight no-stuck safety under funspec preconditions and imported contracts, but applying it upstream additionally requires source equivalence.The lzma decode precondition excludes the raw zero-input call.

7 Related Work

The paper applies VST’s foundational C-verification framework to stateful, resumable decoder machinery while using external agents for proof search and retaining human control over models and specifications. Unlike related agentic reports focused on generating or adapting verified developments, it verifies pre-existing pointer-heavy C bodies against CompCert semantics.

  • VST provides separation-logic verification for C through CompCert semantics, and the paper applies it to stateful, resumable decoder machinery.Adaptive proof search is delegated to external agents while model and contract changes remain under review.
  • Related reports use AI agents for substantial Rocq developments, including adapting a CPS technique and repairing proofs after mutation.These reports concern individual deep proof developments.
  • This work verifies multiple pre-existing, pointer-heavy C functions against CompCert Clight semantics rather than generating new code whose effects remain unverified.

8 Conclusion

The conclusion reports 22 closed semax body theorems for liblzma decoder components, establishing conditional Clight safety and model-relative partial functional correctness. The workflow combined agent-constructed proofs with human-approved semantic changes, and the verification exposed undefined behavior in raw LZMA1 zero-input handling.

  • 22 closed semax body theorems establish Clight safety, including memory safety, and model-relative partial functional correctness under funspec preconditions and imported contracts.
  • The verification exposed undefined behavior in the raw LZMA1 zero-input path.The authors reviewed the manuscript and retain responsibility for it despite LLM assistance.
  • Across 1,595 lzma decode sessions, agents constructed proofs and propagated human-approved revisions while Rocq checked the resulting proof terms.

A The Proving-Subagent Prompt

The proving-subagent prompt constrains each agent to one proof file, immutable definitions and specifications, and explicit compilation and handoff procedures. This preserves attributable, independently checked progress while routing specification changes through human review.

  • Each proving subagent may edit exactly one proof file, preventing parallel interference and making every change attributable.
  • Agents cannot change definitions or lemma statements; when a goal is unprovable, they must diagnose the cause and propose one concrete fix without applying it.
  • Agents read and update a handoff file carrying current state, next steps, and gotchas across sessions.
  • Completed proof steps are retained while unresolved goals remain explicit admits, and the orchestrator independently recompiles before committing validated progress.
  • Subagents use Rocq tools to inspect goals, query the environment, execute tactics, and compile files through the orchestrated workflow.

B An Agent-Reported Specification Gap

A proving agent identified a specification gap in the framing decoder invariant, explained why the state was unreachable in the C code, and proposed a reviewed multi-site strengthening that closed the theorem.

  • Invariant gap: The blocked Compressed1 case involved a child at Lzma1Sized with next sequence Copy, a state admitted by the existing invariant.The Copy disjunct imposed no child-stage constraint.
  • Agent report: The agent reported why the goal was not derivable, why the state was unreachable in the C code, and a candidate fix without applying it.Sized arises through the compressed-chunk path, whereas Copy is selected only by uncompressed control values and leaves the child DecodeReady.
  • Approved refinement: The accepted repair strengthened the Copy disjunct with a stage constraint and sequence alternatives, changing one conjunct into three.The specification remained frozen until owner approval.
  • Propagation: The strengthening imposed obligations on every producer and consumer of the invariant rather than requiring only a local edit.Agents re-established it at nine producer sites and threaded it through additional uncompressed-copy branches.
  • Outcome: The framing body theorem closed with Qed after the strengthened invariant was propagated and the same issue was resolved on uncompressed-copy paths.No proof agent edited the specification itself.

C Separation Lenses for Struct Footprints

Separation lenses regularized reasoning about liblzma’s 29-field decoder struct by isolating individual fields while preserving the remaining footprint as one predicate.

  • Motivation: VST represented the 29-field decoder struct as one deeply nested spatial assertion, although operations typically accessed only one or two fields.The lens technique addressed this mismatch during proof development.
  • Construction: A separation lens combines per-field predicates, a whole-struct predicate parameterized by absent fields, and focus/unfocus lemmas.These components support extracting and reinserting a field’s representation.
  • Operations: The focus operation extracts one field predicate while preserving the remaining fields as a single whole-struct predicate.The unfocus operation reverses this transformation.
  • Effect: Lenses enabled local operations while framing all other fields together, making proof goals more regular and speeding intermediate development.The final proof does not depend on the lenses.

D Proof-Size Measurement Notes

The paper measures proof and generated-code size with postprocessed source counts, parsed Clight layouts, and constructor-based statement counts, while explaining a major dispatch-case discrepancy.

  • Proof counts: Proof-code counts exclude comments and blank lines, and main-lemma measurements run from each Lemma declaration through its terminating Qed.Nested comments and comment delimiters inside string literals are handled correctly.
  • Generated C: Macro-expanded C is counted after preprocessing with clightgen’s definitions and include paths, then cross-checked against regenerated Clight statement counts.Functions are counted from signature through closing brace, excluding header contents.
  • Statement counts: Clight statement counts use constructor counts over generated abstract syntax trees, with lzma decode containing 33 Sreturn nodes and 32 assignments to each listed state variable.Saved range-coder fields each have 64 assignments, including one save and one additional operation described in the passage.
  • Derived measures: The symbolic-execution numerator is divided by code-line counts, while the repeated-block share is based on exact block matching after whitespace normalization.The repeated-block measurement therefore uses textual identity under that normalization.
  • Dispatch comparison: 16,957 extracted lines for Normalize exceed 10,071 for byteidentical IsMatch because Normalize separately handles an eopm case split and re-establishes the full postcondition on exit paths.Normalize uses 3.53, 2.18, and 0.61 proof lines per Clight statement node across the reported cases, versus 4.29 for IsMatch.
Loading 2608.29716v1…