VeriPy: Source-Preserving Verification and Compatibility Checking for Python Components

Updating a verified Python component raises two questions. Does the new implementation satisfy its contract, and does it preserve the behavior that existing callers rely on? These questions need separate answers. Two implementations can satisfy the same contract yet return different values for the same input. A proof of functional correctness alone cannot establish backward compatibility.

We built VeriPy to address both questions while keeping the Python implementation available to native callers. Developers and agents write contracts, loop invariants, termination measures, and proof hooks as Python comments. VeriPy translates supported components into Dafny or Lean, checks auxiliary lemmas, and points unresolved proof obligations back to their source locations. Its relational checker compares successive versions on the inputs admitted by the earlier version.

This approach builds on established work in source annotations and proof erasure. Frama-C integrates analyses around a shared specification language, with its WP plugin providing deductive verification of C contracts. Nagini verifies annotated Python through Viper's permission-based verification infrastructure. VeriPy focuses on sequential components whose Python bodies can be preserved, whose dependencies have explicit models, and whose versions can be compared. Its contribution is a common workflow for functional verification and compatibility checking, evaluated on components from existing repositories.

We evaluated component verification, historical version comparisons, proof reuse during maintenance, and integration with native callers. The examples below show where the workflow succeeds, where proof preparation remains costly, and where the current models cannot support a comparison.

VeriPy verifies an annotated Python component together with an explicit model of its environment. Figure 1 shows how the source reaches the verifier and how diagnostics return to the proof author. Runtime guards and execution comparisons provide additional checks, each with a different role from deductive proof.

Admission and source preservation

VeriPy first obtains type information through basedpyright, then checks whether the selected backend supports the component's syntax and operations. We call this second check admission. A component must pass both checks before verification can proceed. Type checking alone proves no functional contract, and even a supported type may have operations that the backend cannot encode.

Source preservation is checked by comparing executable abstract syntax trees after erasing type annotations. Contracts and proof hooks use the #@ comment syntax and add no execution to the unwrapped function. Extraction adaptations and stronger interface assumptions are recorded separately. For example, some Black components specialize general collection interfaces to builtin lists. Such specialization narrows the verified domain and must not be presented as verification of the original unrestricted interface.

The models operate on exact builtin values or explicitly modeled snapshots. This restriction matters because a Python subclass can override an operation that the model treats as builtin. For framework objects, adapters can snapshot the fields a component uses. Those adapters assume that reads remain stable while the snapshot is constructed.

The same need for explicit models extends to dependencies. A bounded AST evaluator resolves supported forms of module initialization without executing arbitrary initializers. It records constants, dependency operations, exception hierarchies, and registered regular expressions. String reasoning uses a declared Python and Unicode configuration. Our extension studies support Unicode scalar strings but reject lone surrogates. Regular-expression support is limited to the registered patterns studied.

Contracts and checked proof support

Specifications describe preconditions, postconditions, normal returns, modeled exceptions, and entry-state values. Loop invariants and termination measures connect these contracts to iterative code. Named proof hooks invoke auxiliary definitions and lemmas in separate proof files, called sidecars. These lemmas are checked as part of the generated verification artifact rather than accepted as assumptions.

Other verification systems organize executable code and proof differently. Verus separates executable, specification, and proof code in Rust. Aeneas supports Rust verification through functional translation, while Strata provides extensible analysis infrastructure in Lean, including Python analysis through Laurel. In VeriPy, we keep these roles in Python bodies, comment annotations, and checked sidecars. VeriPy's own encoders remain part of its assurance argument, as discussed under Limitations.

VeriPy uses separate direct AST encoders for Dafny and Lean. The Dafny path produces programs and contracts for SMT-backed verification. The Lean path produces executable definitions and propositions checked by Lean's kernel. They share admission and dependency machinery, but their supported features differ. The historical relational checker currently targets Dafny.

VeriPy restricts sidecar declarations, rejects unsupported assumptions, and audits the axioms used by Lean artifacts. Axiom checking alone is insufficient. The frontend must also preserve the hypotheses under which a theorem holds, since a conditional theorem cannot establish an unconditional contract. These checks connect the proposition verified by the backend to the guarantee reported for the Python component.

Native execution and evidence

Optional guards wrap the original Python body with the implemented type, dependency, alias, and precondition checks. Some integrations copy inputs into snapshots. Others preserve mutation and permitted aliasing, as PyPNG's in-place scanline operations require. VeriPy can generate a guard before a proof succeeds, so a guarded component must still be distinguished from a verified one.

To look for translation errors, we compare native observations with executable translations. The generic harness uses Hypothesis. Individual studies also use deterministic inputs, upstream tests, independent oracles, and kernel-reduced Lean executions. CrossHair checks Python contracts through symbolic execution and counterexample search, a complementary approach to the execution comparisons used here. Our checks can expose disagreements between Python and its model. They cannot prove the translator correct. A backend proof applies to the translated model, and connecting that result to Python execution still depends on the frontend, semantic models, dependencies, and runtime assumptions.

Consider a contract that requires a return value to lie within a range. Two versions may return different values within that range and both pass verification. For a caller that depends on the exact value, the update still changes behavior.

VeriPy checks that the new version continues to admit every input admitted by the old version and produces equal declared observations. For the terminating components evaluated here, those observations are typed return values and modeled exception tags. Requiring the old inputs to remain valid prevents a new version from passing simply by excluding inputs on which the versions disagree.

To make this comparison, the checker encodes each version in a separate namespace and constructs a sequential relational wrapper. It verifies the two bodies, their sidecars, and the wrapper together, following the established use of product programs for relational verification. Exact functional contracts and checked relation lemmas supply the facts needed to compare the calls. The checker does not infer alignments between arbitrary loops.

Related work applies self-composition to different verification settings. RPP combines static and dynamic verification of relational properties of C programs. Product Programs in the Wild constructs products at an intermediate verification language level for information flow security. VeriPy applies relational reasoning to version compatibility over selected Python observations. The product construction still depends on the correctness of each component's encoding.

Scope and verdicts

The current implementation requires matching parameter names, kinds, types, return types, and admitted immutable literal defaults. Supported record snapshots are related through generated field-preserving maps. Exception hierarchies must agree sufficiently to compare their modeled tags. Changed defaults, variadic interfaces, and relational mutable-buffer operations remain unsupported.

The relation excludes exception messages, tracebacks, object identity, resource consumption, and concurrent interference. It is a guarantee about selected observations at a callable boundary, not compatibility of an entire library release.

A comparison can have four outcomes. VeriPy reports proved compatible when the product proof succeeds, or counterexample when a concrete native input produces different observations. If the proof fails or exhausts its budget without a witness, the result is inconclusive. A comparison that the pipeline cannot construct is unsupported. Replaying inputs can supplement these results, but agreement on a finite set of executions does not establish compatibility for every admitted input.

The Django base36 example

Django's int_to_base36 illustrates compatibility across different algorithms. Password-reset-token code uses the function to encode a timestamp. The earlier implementation emits digits from left to right, while the later implementation repeatedly applies divmod and prepends digits. The required relation preserves the exact base36 string for nonnegative integers and ValueError for negative inputs.

We prove the relation using a checked definition of canonical base36 encoding. For the later implementation, an invariant connects the original input to the remaining quotient and accumulated suffix. A decreasing measure establishes termination, and a proof hook invokes a checked encoding-step lemma before the next executable update. The old implementation has its own invariants and proof support. Because both contracts specify the exact encoding, the product can establish equal outcomes without matching the two loop structures.

The Dafny product proves compatibility between the two implementations. The comparison uses a Python 3 specialization that omits an unreachable Python 2 branch, so the guarantee applies to that specialization.

A separate integration study placed the guarded converter in Django 6.0's password-reset-token code. Six timestamp comparisons produced identical tokens, with execution checks covering 1,957 native, guarded, and compiled cases. This study tests the converter in a real caller. It does not establish authentication security or compatibility of the Django release.

To try VeriPy, start with a small typed function and an explicit contract. The installation guide requires Python 3.11 or newer and installation from source. The package named veripy on PyPI is a different project. In a POSIX shell, create an isolated environment from the repository root.

git clone https://github.com/astrio-labs/veripy.git
cd veripy
python -m venv .venv
source .venv/bin/activate
python -m pip install -e '.[dev]'

The Python installation does not install a proof backend. Choose Dafny or Lean for functional verification. The Dafny setup guide uses Dafny 4.11.0, with the .NET 8 SDK required for the documented .NET tool installation. The Lean setup guide uses Lean 4.33.1 installed through elan, without Mathlib. Make the selected backend executable available on your PATH.

Verify with Dafny

Save the following example as component.py. The comment states that the returned value must equal the input plus one. It leaves the executable Python body unchanged.

#@ ensures result == x + 1
def increment(x: int) -> int:
    return x + 1

Run the static checks, then ask the default Dafny backend to verify the contract.

veripy check component.py
veripy verify component.py --time-limit 30 --outdir build/component-dafny

For a larger component, add preconditions, loop invariants, and termination measures using the annotation syntax. When an obligation remains unresolved, use the source diagnostics to refine annotations or checked auxiliary lemmas and rerun verification. A failed proof or timeout is not, by itself, a counterexample. Keep changes in the Python source and checked proof support so that the verified artifact continues to correspond to the program.

Verify with Lean

The Lean backend checks contracts against generated Lean definitions, using backend-specific proof support where needed. To run a maintained example with its checked sidecar, verify the SGLang planner from the repository root.

python -m veripy verify case_studies/sglang/live_planner.py --backend lean --json build/sglang-lean/result.json --time-limit 900

The current CLI requires --json for non-default backends. Use a fresh output directory for each run. Auxiliary Lean proofs live beside the Python source in NAME.proofs.lean files. The Python body and supported contracts can remain the same across backends, but Dafny lemmas must be replaced with Lean proof support. Consult the Lean guide for supported constructs and proof hooks. In particular, ghost_ensures remains Dafny-only.

Compare versions

Version compatibility checking currently uses Dafny, including for components that have separate Lean functional proofs. The repository includes the annotated sources and proof support for the Django base36 comparison described above. Run it from the repository root, choosing a fresh output directory for each attempt.

python case_studies/tools/run_compatibility.py --projects django --out build/django-compatibility

To compare your own components, follow the callable compatibility guide. Supply the old and new annotated implementations and their required proof support. The checker evaluates whether old inputs remain admitted and whether modeled outcomes agree. Read the resulting verdict as proved compatible, a witnessed behavioral difference, unsupported, or inconclusive.

We evaluated functional verification, historical compatibility, proof reuse, and runtime integration using components from existing repositories. Annotations and proofs were developed interactively. The components were selected for their practical roles and are not a representative sample of Python software.

Functional verification

Both Dafny 4.11.0 and Lean 4.33.1 verified all 25 proof units from seven repositories using identical annotated Python sources. Some units compose others in the study, so the count includes overlapping code rather than 25 independent programs.

The contracts capture different properties in each repository. For Black range composition, we verify exact ordered outputs. The SGLang planner specifies allocation lengths and reserve conditions, while the PyTorch component specifies shard-overlap behavior. Django requires exact base36 encoding, and the vLLM padding component specifies an optimum with a tie-breaking rule. These contracts differ in strength, and a successful proof establishes only the properties stated in the contract.

Small Python functions can still require substantial proof support. CPython's time parser has 37 Python code lines and 34 postcondition clauses, but its Lean sidecar requires 976 nonblank, noncomment lines. That proof covers the helper's parsing behavior, not complete ISO validation or equivalence to a historical parser. Proof size and verification time do not capture the full preparation cost. Human authoring time and total model usage were not measured.

Historical compatibility

The initial compatibility study compared one callable across two versions in each of ten repositories. Changed implementations test behavioral preservation across updates, while unchanged implementations serve as controls.

Four comparisons produced proofs, covering two changed bodies and two unchanged-body controls. Black removes a redundant emptiness check over an exact two-integer tuple. Django is the base36 algorithm change described above. Each proof concerns the selected callable, so it cannot establish compatibility of the surrounding release.

Packaging produces three concrete native witnesses. With validation enabled, name="foo\n" changes from a returned string to InvalidName. Reordering lowercase conversion and separator replacement also changes Greek final sigma behavior. A witnessed difference establishes incompatibility under the declared observations, but need not indicate an unintended defect.

The python-stdnum comparison is inconclusive because its range and error contracts do not determine the exact arbitrary-alphabet checksum. They therefore provide insufficient information to prove equal results. A proof for a narrower decimal checksum does not resolve that comparison. In an extension of the initial study, record-snapshot support enabled compatibility proofs for the unchanged SGLang and PyTorch components. The table reports the initial study, before that extension.

Controlled maintenance

An existing proof may contain useful material for verifying an update. We studied whether giving an agent access to that material helped it prove functional correctness and compatibility. This question complements work on proof assistance such as DafnyBench, which evaluates completion of missing proof hints, and DafnyPro, which combines invariant pruning and hint augmentation while preserving executable logic. We did not compare VeriPy directly with either system.

The experiment used twelve agent-authored updates to six human-reviewed components, with the original proofs fixed before update generation. The original functions contain 5 to 17 code lines, and the updates are synthetic rather than upstream changes. Each update was evaluated twice per condition, giving 24 trials in each group. Both groups used GPT-6 Astra at medium reasoning with the same sources, contracts, public relations, checker, and three-response budget. The reuse group also received the original proof annotations and checked helpers. The rebuild group received the fixed specification. Four transformations without private proof support served as controls.

The reuse arm completed more proofs, but the entire completion gap came from Packaging. Its old proof also revealed backend regular-expression APIs. In a separate post-hoc check, we gave the public regex definitions to both arms. Both then passed all four trials in one response each. This finding prevents us from attributing the original gap to a general benefit from lemma reuse. The repetitions are also not independent samples, and response counts depend on when a run succeeds or stops.

A follow-up experiment on the Django rewrite found no advantage from old proof access. Both groups proved the update in both repetitions with equal response counts. Extending the study to fourteen additional upstream changes across seven repositories was limited by proof preparation. None had an adequate proof of the earlier implementation to support a maintenance comparison. The study therefore provides no estimate of the benefit of proof reuse on those changes.

Runtime integration

We integrated SGLang's guarded allocation planner into an installed EAGLE3 decode path using Qwen3-1.7B on one A10G. Ten matched process pairs evaluated requested batch sizes 1, 8, 32, and 128. Paired geometric-mean latency changes ranged from −0.690% to +0.839%, and all family-adjusted 98.75% bootstrap intervals included zero. These measurements do not establish negligible overhead because we had not declared an equivalence margin. Generated text matched across 400 measured calls.

Runtime overhead depends on the component and the checks required at its boundary. For Black's size-32 normalization, median execution time rose from 3.22 microseconds natively to 69.51 microseconds with the guard. Copying, deep checks, and precondition evaluation can add substantial work around a small function. This measurement and the GPU experiment concern different workloads, so they cannot be pooled into a performance ranking.

We have not proved end-to-end soundness of the complete Python encoder. The assurance argument depends on admission checks, dependency resolution, semantic models, preservation of specification hypotheses, and the connection between checked artifacts and reported source. Checking both backends and comparing executions helps find errors, but an error in shared frontend code can affect both translations.

VeriPy supports a declared subset of Python. Arbitrary objects, reflection, unrestricted regular expressions, resource exhaustion, and concurrent mutation remain outside scope. Integration also leaves assumptions that must be checked for each caller. The PyTorch overlap proofs require positive shard widths, with native fallback retained for zero-size cases. Black's verified components rely on match records supplied by a native diff engine that they do not verify. Runtime guards enforce only their implemented checks.

The evaluation reflects selected, manually annotated components, including overlapping proof units. Maintenance trials use small prepared functions and one model family. The runtime experiment covers one GPU host and workload family. We report neither a head-to-head verifier comparison nor a total development cost estimate. Human and model review can identify specification errors, but neither certifies that a contract captures everything a caller needs.

For each verified component, readers therefore need the contract, admitted inputs, preserved observations, and assumptions that connect the model to execution. A successful verifier run alone does not supply that context.

VeriPy remains an ongoing research project. We next plan to extend compatibility checking to mutable buffers, aliasing, and interfaces the checker cannot yet admit. Each extension needs an explicit model of the behavior it preserves and checks that connect that model to Python execution.

The preparation failures in the maintenance study also leave an unresolved question. How much work is needed to make proof reuse practical for previously unseen upstream changes? We plan to measure specification and proof authoring costs alongside completion, including cases that fail during preparation. Separating access to old proof material from access to public library information will help clarify what any improvement comes from.

We also plan to formalize translation obligations and expand adversarial checks of the assumptions connecting backend proofs to Python execution. Runtime guards need evaluation across broader workloads, with equivalence margins specified in advance when testing whether overhead is negligible.

We thank Todd Schmid, Jules Jacobs, and Wojciech Różowski for their advice and guidance, and Nada Amin and Robert Joseph George for early discussions.