Voblint

A Verified Goblint-Style Static Analysis Pipeline in Isabelle/HOL

Master's thesis. Manuel Lerchner, supervised by @AlexandraGrass

What is Voblint?

Voblint is a context-sensitive static analyzer for VIMP, a small C-like language with integer variables and recursive procedures. Modeled on Goblint, it builds a control-flow graph, derives a system of equations, and solves them with a verified generic solver. Its soundness proof in Isabelle/HOL connects the parsed program to the analyzer's reported answers.

The proof is modular: domains, analyses, and calling-context policies each establish their own soundness obligations. Activation traces connect individual procedure activations to the contexts used by the analysis. The analyzer is exported to OCaml and runs in a command-line tool and a browser playground.

What is verified?

Whenever the analyzer returns a report, its abstract states cover every state that a finite execution of the program reaches. The reported verdicts follow from that coverage:

\underbrace{(\mathit{main}, s_0, [\,]) \to_p^{*} (r, s, \mathit{fs})}_{\text{source run}}
\;\Longrightarrow\;
\underbrace{\exists v.\; (r, s, \mathit{fs}) \rhd v}_{\text{observed at a node}}
\;\wedge\;
\forall v.\; (r, s, \mathit{fs}) \rhd v \Longrightarrow
\underbrace{s \in \mathcal{C}(v)}_{\text{collecting semantics}}
\;\wedge\;
\underbrace{\mathcal{C}(v) \subseteq [\![\, \mathit{res} \,]\!]_{v}}_{\text{analysis soundness}}
\;\wedge\;
\underbrace{[\![\, \mathit{res} \,]\!]_{v} \subseteq \mathcal{V}_{\mathit{res}}(v)}_{\text{verdict soundness}}

Read the formula from left to right: a source execution reaches a state $s$; that state corresponds to a graph node $v$; the analysis covers all reachable states there; and its definite verdicts hold for those states. The analysis may include states that no execution reaches, so it can report uncertainty.

For example, PROVED means an assertion holds whenever execution reaches it. DEAD means the point is unreachable. REFUTED means the assertion is false whenever reached; it does not establish that any execution reaches it.

The guarantee assumes an accepted program and configuration and a terminating solver run. Solver termination is not proved for every program. Parsing, code generation, the target-language toolchain, and presentation of results remain outside the proof.

The headline theorem gives the precise statement and its connection to the Isabelle development.

Interactive proof map

Explore the interactive proof map as a corpus wheel or treemap. Blocks group entities by session and theory; their area reflects entity counts, including generated declarations. Colors follow the session dependency layers. Zoom in to inspect entities and open their Isabelle documentation.

Running Voblint

Voblint programs are written in VIMP, a small IMP-style language with __voblint_check(cond) assertions:

fun main() {
    x = 0;
    while (x < 10) {
        x = x + 1;
    }
    __voblint_check(0 < x);
}

$ pixi run voblint --analysis interval tests/regression/02-control-flow/precision/02-while_loop.vimp
tests/regression/02-control-flow/precision/02-while_loop.vimp [interval]

Arithmetic diagnostics
None

Assertion checks
Location  Point  Condition  Verdict  State
--------  -----  ---------  -------  -------------------
8:3       pp3    0 < x      PROVED   interval: x=[10,10]

The browser playground runs the same generated analyzer on a program you edit, with no server involved. Verdicts and value hints appear in the source, the cursor's statement shows its state in every context, and the solved graph draws one box per procedure and context. To explore a local program there, add --playground: it opens the playground with the file and the given settings, or those of its // PARAM: header, instead of analyzing it locally.

pixi run voblint --analysis interval --context entry-state my_program.vimp --playground

--context none|entry-state|call-string selects the analysis context, --globals the update rule for side-effected globals, and --program-globals flow-sensitive|flow-insensitive whether a program's globals travel with each point's state or each live at its own global unknown, read only by the points that mention it; both placements carry the same soundness theorem. pixi run voblint --help lists every flag. --graph-snapshot prints the solved graph as deterministic text and --parse-only checks syntax. docs/CLI_DESIGN.md describes the CLI trust boundary and docs/CHECK_ARCHITECTURE.md how a result becomes a report.

--trace also writes the solver's steps to stderr: per call, the context it is routed to, what the callee's entry reads from its seed, and which publications restart the caller. --verbose lists every step in a Goblint-aligned tracing vocabulary (%%% iter: begin iterate ...; the mapping table in docs/CLI_DESIGN.md records every difference), --trace-sys iter,side selects subsystems, --format jsonl emits JSON Lines and --output FILE writes to a file; standard output stays the same. The playground's run_voblint: call and answer panel shows the full (--verbose) trace under the call and its answer, colored by step and folded by query, with downloads of the whole text and of its JSON Lines form. Three layers: the solver result is the exported computation of proved equations, and a traced run calls run_voblint_traced, whose trace calls come from code equations proved equal to the untraced ones (an untraced run reaches no hook); the trace is an unverified observation of that computation, through a code_printing mapping of trace_event to an OCaml hook that returns unit, swallows exceptions and never touches solver state, so it cannot feed back; the replay and animation are an unverified visualization of the trace (docs/CLI_DESIGN.md).

pixi run voblint --analysis interval --context entry-state --trace docs/readme-figures/contexts.vimp

The playground's Solve replay section steps through the same solve on the graph, with the verbose trace beside it: the value each unknown holds, the seed each call publishes its entry state into, the stack of open queries and the edge each query follows backward from the exit, with the stable set, destabilization cascades, widening points and influence edges drawn on the graph and the routes and counters below it. One reducer folds the run's JSON Lines trace into every state it shows. node scripts/capture_readme_figures.mjs solve-replay regenerates the animation below from the playground.

Arithmetic diagnostics

Every analysis also checks the divisors of / and % against the solved state before the statement. A divisor that may be zero is a warning; one that is zero in every live context is an error. Safe operations and unreachable points report nothing, and diagnostics never change the exit code.

The traversal covers assignments, guards, call arguments, returns, min/max and checks, nested arithmetic included, and both operands of && and ||. It is a diagnostic policy over VIMP's total expressions: execution still uses a / 0 = 0 and a % 0 = a. “Possible” means the abstraction cannot exclude zero, not that a zero-divisor execution exists; an error does not prove its point reachable. The arithmetic fixtures pin the findings and describe the expectation syntax.

What Voblint proves

For every selection of analyses, globals rule and context policy, the report run_voblint returns is sound for every execution of the program: whenever an execution reaches a program point, some state the report holds there describes its store, and every PROVED or REFUTED verdict there is correct for it. The theorems are stated about the same run_voblint that is exported to OCaml and runs in the CLI and the playground.

"Every execution" is made precise by an activation-trace collecting semantics. A valid_activation_trace trace records one procedure activation's view of a run, and node_collect gathers every store such traces hold at each CFG node, adapting thread-modular local traces (see Foundations) from threads to procedure activations.

The headline theorem

run_voblint_source_sound relates any finite source execution to the report, at every CFG node the execution is observed at:

theorem run_voblint_source_sound:
  fixes p :: imp_prog and s0 s :: store
  defines "𝒢 ≡ declared_global p" and "Π ≡ prog_table p" and "g ≡ prog_cfg p"
  assumes s0: "s0 ∈ cinit_stores 𝒢"
      and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, frs)"
      and ans: "run_voblint config p = Analysed res"
  shows "(∃v. p, s0 ⊢ (residual, s, frs) ⊳ v)
       ∧ (∀v. p, s0 ⊢ (residual, s, frs) ⊳ v ⟶
                s ∈ 𝒞⇘𝒢,g,cinit_stores 𝒢⇙ v
              ∧ s ∈ ℛ⇘res⇙ v
              ∧ s ∈ 𝒱⇘res⇙ v)"

Premise	Meaning
s0	Initial store. Declared globals start at 0; locals are unconstrained.
run	Any finite execution prefix from main; the program need not terminate.
ans	run_voblint accepted the configuration and the program, and its solve finished.

→⇩p⇧* is psteps, ⊳ is at_node, and 𝒞, ℛ⇘res⇙ v and 𝒱 are node_collect, report_sem and verdict_stores; the notation table lists each symbol.

Conclusion	Guarantee
∃v. … ⊳ v	The reached configuration is observed at some CFG node.
s ∈ 𝒞⇘𝒢,g,cinit_stores 𝒢⇙ v	At every such v, a valid activation trace reaches v with store s.
s ∈ ℛ⇘res⇙ v	Some state the report holds at v, under one of its contexts, describes s.
s ∈ 𝒱⇘res⇙ v	Every PROVED or REFUTED verdict at v holds for s.

A residual command alone does not determine its node, since equal commands occur at different places. at_node therefore reads the node off the program's elaboration elab_pt, which annotates every statement with the nodes the compiler emits for it and compiles to the same graph (compile_prog_elab_pt). p, s0 ⊢ (residual, s, frs) ⊳ v holds when some run of the elaboration from s0 reaches an annotated configuration that erases to the source one, names v (point, csim_point_compile_prog) and is related to v by the compiler's simulation with the same store. Erased, the simulation relates the source configuration to v too (at_node_csim). The relation is not functional: a configuration reachable along two paths can be observed at two nodes, and the second half of the theorem covers every one of them. The elaboration is used only in the proof, and run_voblint runs the program as written.

config names a nonempty list of distinct analyses among Sign, Interval, Parity, Congruence, Int and Order, run together, one of the globals rules, and one context policy: no contexts, entry states, or call strings of any length.

The theorem concludes membership of the reached store in all three sets. The inclusions between the sets are separate theorems about a successful analyzer run: 𝒞 v ⊆ ℛ⇘res⇙ v needs the run that built the report (run_voblint_covers), and ℛ⇘res⇙ v ⊆ 𝒱⇘res⇙ v holds for the report alone (analysis_report_verdicts_sound).

A source residual alone need not name a single CFG node. In if (b) { x = 1; } else { x = 1; }, the residual x = 1 is the same command in both branches, but the two branches compile to different nodes. The elaboration gives each occurrence its own annotation, so that the annotated residual determines its node (csim_point_compile_prog). Every run of the program as written lifts to an annotated run (psteps_lift). at_node quantifies existentially over the annotated command and the stack, and v = point c is fixed by that command. Contexts remain existential, because entry-state routing may admit several contexts for one activation.

Checks, dead code and arithmetic

Results in the same theory specialise the guarantee to what the report shows:

• run_voblint_check_sound: when an execution is about to run a check, the report lists a row under that check's label at a node reached with the current store, the row is not DEAD, and a definite verdict is correct. run_voblint_labelled_check_sound adds that, when no two rows share a label, every row carrying the label is that row.
• run_voblint_dead_unreached: no execution reaches a DEAD point; run_voblint_dead_check_unreached states it for a DEAD check row.
• run_voblint_arithmetic_safe: at a reachable point with no arithmetic diagnostic, every divisor in the point's expressions is nonzero in every store that reaches it.
• run_voblint_arithmetic_refuted: the divisor of an error is zero in every store that reaches its point.

theorem run_voblint_report_contract:
  assumes "run_voblint config p = Analysed res"
  shows "valid_config config" "wf_program_compile_input_exec p"
    and "report_config res = config" "report_cfg res = prog_cfg p"
    and "well_formed_report res" "sound_report p res"

theorem run_voblint_check_sound:
  fixes p :: imp_prog and s0 s :: store
  defines "𝒢 ≡ declared_global p" and "Π ≡ prog_table p" and "g ≡ prog_cfg p"
  assumes s0: "s0 ∈ cinit_stores 𝒢"
      and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, frs)"
      and chk: "next_check residual = Some (l, e)"
      and ans: "run_voblint config p = Analysed res"
  shows "∃c ∈ set (report_checks res). check_label c = l ∧ check_exp c = e
           ∧ s ∈ 𝒞⇘𝒢,g,cinit_stores 𝒢⇙ (check_point c)
           ∧ check_verdict c ≠ Dead
           ∧ (check_verdict c = Decided Check_Proved ⟶ truthy (⟦e⟧⇩e s))
           ∧ (check_verdict c = Decided Check_Refuted ⟶ ¬ truthy (⟦e⟧⇩e s))"

corollary run_voblint_dead_unreached:
  assumes "run_voblint config p = Analysed res" and "DEAD res v"
  shows "𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v = {}"

theorem run_voblint_arithmetic_safe:
  assumes "run_voblint config p = Analysed res"
      and "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v"
      and "∀d ∈ set (report_diagnostics res). diagnostic_point d ≠ v"
  shows "arithmetic_safe_at (prog_cfg p) v s"

theorem run_voblint_arithmetic_refuted:
  assumes "run_voblint config p = Analysed res"
      and "d ∈ set (report_diagnostics res)" and "diagnostic_verdict d = Check_Refuted"
      and "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ (diagnostic_point d)"
  shows "⟦arithmetic_divisor (diagnostic_obligation d)⟧⇩e s = 0"

Limits

The result is partial correctness. run_voblint runs the executable solver, which answers only where the solve terminates, so the theorems need no termination premise; nothing proves that the solve terminates for every program, and where it does not, the analyzer gives no answer. Neither PROVED nor REFUTED establishes that its point is reachable, so REFUTED is not a verified counterexample. DEAD is the only reachability claim: no covered execution reaches the point. The converse does not hold: a point no execution reaches need not be DEAD.

Covered by the proof	Outside the proof
VIMP execution from an already-constructed AST	Solver termination for arbitrary programs
Compilation to the procedure-aware CFG	Lexing and parsing
Equation generation and the computed post-solution	Isabelle code generation, the OCaml compiler and runtime
The report's states, check rows under their labels, arithmetic safety at quiet points, zero divisors at errors	That a check's label is its source position; diagnostic positions; rendered graphs and state strings; the playground
	Completeness and precision

Example_End_To_End_Certificate evaluates the headline theorem's answer for one Int program with call-string contexts, so the theorem is not vacuous. docs/THEOREM_MAP.md lists the lower-level statements.

Notation

Theorem statements use a few symbols the theories declare. Each name links to its declaration.

Symbol	Reads as	Isabelle	Meaning
𝒢,Π ⊢ c →p c' / 𝒢,Π ⊢ c →p* c'	c steps to c′	pstep / psteps	one small step of a source configuration (command, store, frame stack) under procedure table Π; the starred arrow is its reflexive-transitive closure
p,s0 ⊢ c ⊳ v	from s₀, c is observed at node v in p	at_node	some run of the elaboration of program p from store s₀ reaches an annotated configuration that erases to c, names node v of the compiled graph and is related to v by the simulation; a configuration reachable along two paths can be observed at two nodes
𝒢	the global-variable classifier	declared_global	the predicate on variable names that marks the globals; a program supplies it from its global declarations, and the theorems take it as a parameter
𝒯𝒢,g,SWithin activation_coverage, the fixed parameters are omitted: 𝒯	the valid activation traces of g from S	valid_activation_trace	the activation traces of graph g from initial stores S

Reading a result

Each figure is a playground run; the link under it opens the same program and settings.

The gain does not come from a better interval transfer. Sign and Interval invert + conservatively, so the guard y + 1 == 3 tells them nothing about y. Parity inverts it and learns only that y is even. Congruence, the fourth component, inverts + precisely enough to prove the check on its own. Inside int, the reduction re-derives the Sign, Interval and Parity views from the operand Congruence tightened (Int_Backward.thy, Int_Refinement.thy).

The generic D/G framework

Analyses are factored the way Goblint factors them: D holds the abstract facts attached to program points, G the information published and consumed across points. The framework's interface is dg_spec, the Isabelle counterpart of Goblint's Spec (transfer, entry, combine and communication). Equation generation with context routing, solver integration and the lifting to source-level soundness are proved once, for any dg_spec with an analysis_contract relating it to concrete stores; see src/Abstract_Interpreter/Framework/README.md. Specifications that read or publish globals of their own, such as the relational rel_order_spec, instantiate dg_spec directly.

Every analysis selectable through run_voblint enters through a smaller interface, a local_spec: one transfer per edge kind plus entry and combine, over local state only, with the soundness condition sound_local_spec. dg_spec_of lifts it to a dg_spec, and dg_spec_of_contract supplies the contract. With flow-insensitive program globals, keyed_split_spec wraps that specification so each edge reads only the globals its expressions mention and publishes only the globals it may assign, each at its own unknown, and keyed_split_contract carries the contract over.

A numeric domain supplies one record of value operations, nonrelational_ops: an abstract evaluator, the comparison queries < and ==, backward refinement operators, min/max and top. It proves one certificate, sound_nonrelational_ops; Sign, Interval, Parity and Congruence also prove their operations monotone. Everything else is derived from that record: the guard filter and branch transfer, the check classifier, the assignment and entry transfers, and their executable versions. Abstract and executable versions come from the same operations and agree on live stores, so there is no second implementation to prove equal. One rule, dg_analysis_execI, discharges the registration's transfer and classifier obligations from the certificate. The relational Order analysis writes its local_spec by hand (order_spec). Deriving transfer functions from certified value operations follows Nipkow's Isabelle abstract interpreter (see Foundations).

Each domain registers itself in a few lines per context policy, by interpreting the locales of Nonrel_Registration. A new numeric domain needs its lattice with widening and narrowing, its concretization, the certified operation record, a lemma that the initial state covers the initial stores, these registrations, and a field in the combined state (MCP_Carrier). The CLI's analysis names are added by hand as well. No step needs source-level reasoning.

Building

Requirements: Isabelle2025-2, an AFP checkout, pixi, and OCaml via opam for the CLI.

./scripts/setup.sh                             # pixi, OCaml and developer tooling
pixi run vendor-init                           # fetch the TD solver submodule
AFP=/path/to/afp/thys pixi run isabelle-build  # check the formalization

On a fresh clone without parent heaps, run pixi run isabelle-bootstrap first, with the same AFP setting. pixi run isar-check checks ROOT entries, unfinished proofs, theory syntax and formatting with isar-tools, without Isabelle or the AFP. pixi task list lists everything else.

The vendored solver is pinned to a private fork of stilscher/td-verification; CI needs a SUBMODULES_TOKEN secret to clone it. Making that fork public is the outstanding step for a fully reproducible artifact.

Foundations

• Goblint (GitHub): modular interprocedural abstract interpretation and the D/G architecture.
• Abstract Interpretation of Annotated Commands (ITP 2012): reusable abstract interpretation in Isabelle/HOL.
• The Top-Down Solver Verified (CAV 2024): the vendored executable verified solver.
• Mixed Flow-Sensitive Static Analysis: Engineering Modularity (FM 2026).
• Data Race Detection by Digest-Driven Abstract Interpretation (arXiv:2511.11055): thread-modular local-trace semantics of a multithreaded program. Voblint's activation traces (src/Program_Model/CFG/Collecting/) adapt its shape to procedure activations of a sequential run.

Documentation

Document	Contents
AGENTS.md	Project contract, style rules, working agreements
docs/PROOF_OVERVIEW.md	Proof architecture and intended claims
docs/THEOREM_MAP.md	Thesis claims mapped to checked Isabelle theorems
docs/GLOSSARY.md	Terminology and defining layers
docs/VERIFICATION_CHAIN_AND_TRUST_BOUNDARY.md	What is proved, what is trusted
docs/GOBLINT_ALIGNMENT_REGISTER.md	Where this formalization differs from upstream Goblint, and why
docs/ISABELLE_AGENT_NOTES.md	Build commands, agent-assisted development (I/Q, I/R), ./scripts/setup.sh
docs/ROADMAP.md, docs/NON_GOALS.md

License

Voblint is available under the BSD-3-Clause license. Vendored dependencies retain their own licenses.