← All papers
First page of Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology

Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology

Halley Young

cs.PL Mar 27, 2026 · v1
Key metatheorems (soundness, descent theorem, Mayer-Vietoris localization, fixed-point convergence) are mechanized in 1,259 lines of Lean 4 with Mathlib.
We present a framework in which program analysis – type checking, bug finding, and equivalence verification – is organized as computing the Čech cohomology of a semantic presheaf over a program's site category. The presheaf assigns refinement-type information to observation sites and restricts it along data-flow morphisms. The cohomology group $H^{0}$ is the space of globally consistent typings. The first cohomology group $H^{1}$ classifies gluing obstructions – bugs, type errors, and equivalence failures – each localized to a specific pair of disagreeing sites. This formulation yields three concrete results unavailable in prior work: (1) the rank of $H^1$ over $F_{2}$ counts the minimum independent fixes; (2) $H_{1}(U, Iso) = 0$ is sound and complete for behavioral equivalence; (3) Mayer-Vietoris enables compositional, incremental obstruction counting. We implement the framework in Deppy, a Python analysis tool, and evaluate it on a suite of 375 benchmarks: 133 bug-detection programs, 134 equivalence pairs, and 108 specification-satisfaction checks. Deppy achieves {100% bug-detection recall} (69% precision, F1 = 81%), 99% equivalence accuracy with zero false equivalences, and 98% spec accuracy with zero false satisfactions – outperforming mypy and pyright, which report zero findings on unannotated code. The analysis models Python semantics as algebraic geometry: variables live on the generic fiber (non-None) unless on the closed nullable subscheme, integers form Spec($\mathbb{Z}$) with no bounded section (no overflow), and short-circuit evaluation defines an open-set topology on the presheaf.

Program analyses such as type checking, bug finding and equivalence checking all combine local facts into global conclusions. The authors seek a single mathematical framework for this local-to-global reasoning that also supports counting, localizing and composing errors.

Program analysis is modeled as computing the Čech cohomology of a semantic presheaf of refinement types over a program site category whose morphisms are data-flow edges. H^0 captures globally consistent typings and H^1 classifies gluing obstructions such as bugs and equivalence failures. The framework is implemented in Deppy, a Python analyzer that uses Z3 to check agreement on overlaps. Its metatheory (soundness, the H^0 characterization, the descent theorem, Mayer-Vietoris and convergence) is mechanized in Lean 4 with Mathlib across 7 modules.

On 375 benchmarks, Deppy reaches 100% bug-detection recall (69% precision, F1 81%), 99% equivalence accuracy with no false equivalences, and 98% specification accuracy. mypy and pyright report zero findings on the same unannotated code.

TaskCorrect / TotalNotes
Bug detection (133)—P 69%, R 100%, F1 81%
Equivalence (134)133 / 134 (99%)0 false equivalences
Spec satisfaction (108)106 / 108 (98%)0 false satisfactions
Deppy accuracy across benchmark tasks