From Programs to Proof Pipelines

Post 13 · Phase 3 — Verification

Throughout this series, we have built up a system with facts, rules, effects, invariants, processes, spatial structure, resources, and universes.

At each step, we defined what is valid, what must hold, and what can change.

But defining correctness is not the same as checking it. We now turn to the question: how does Spine actually verify the properties we have described?

The State of Verification

Powerful verification tools already exist.

Z3 is a theorem prover that can check whether logical constraints are satisfiable — whether a set of conditions can ever be violated.

TLA+ is a specification language for reasoning about state machines — temporal sequences of transitions and the properties they preserve.

PRISM is a probabilistic model checker — it can verify properties of systems with uncertainty, where outcomes have likelihoods rather than certainties.

Each of these tools is well-established and individually capable.

But more exists. mCRL2 is a toolset for analyzing concurrent processes — it can verify behavioral properties like deadlock freedom, liveness, and behavioral equivalence. BigraphER is a tool for reasoning about spatial structure and reconfiguration — it can check properties of systems where nesting, containment, and movement matter.

Together, these tools cover a remarkable range: logical constraints, temporal behavior, probabilistic properties, concurrent processes, and spatial structure.

The problem is that they exist in isolation.

A Fragmented Landscape

In practice, using these tools requires translating your system into each tool's own language, maintaining parallel representations, and reconciling the results.

The developer who writes the business logic is rarely the same person who writes the TLA+ specification. The Z3 encoding is yet another artifact. The probabilistic model is separate again. The process algebra model and the spatial configuration exist in their own worlds entirely.

As a result, verification is something most projects either skip entirely or apply only at the most critical points, if at all.

The problem is not that the tools are weak. It is that the path from program to proof is too long.

Verification as Part of Compilation

Spine takes a different approach.

Verification is not a separate phase. It is part of compilation.

Because Spine programs already express facts, constraints, invariants, and effects explicitly, the compiler has everything it needs to generate verification targets automatically.

The developer does not write a Z3 encoding. The compiler extracts one from the system's constraints. The developer does not maintain a TLA+ specification. The compiler derives one from the system's rules and transitions. Process models are extracted the same way.

What Gets Checked

Return to our Asset System.

We have defined:

From these definitions, the compiler can extract several verification obligations:

Constraint Satisfiability (Z3)

Can the invariant be violated? Is there any assignment of facts that satisfies all rules but breaks ownership uniqueness? Z3 checks this by searching for a counterexample. If none exists, the invariant holds.

Temporal Properties (TLA+)

Does every sequence of valid transitions preserve the invariant? Can the system reach a state where two agents own the same asset? TLA+ explores the state space of all possible evolutions and checks that the property holds on every path.

Process Properties (mCRL2)

Can two concurrent processes deadlock? Does the approval workflow eventually produce a response for every request? Are two implementations of the same service behaviorally equivalent? mCRL2 analyzes the process structure extracted from the system's concurrent components.

Planned: Probabilistic and Spatial Properties

Two additional verification dimensions are under development. Probabilistic properties (via PRISM) would check whether the probability of reaching an invalid state remains below a threshold. Spatial properties (via BigraphER) would verify containment invariants and spatial reconfiguration. The modeling constructs for both exist in Spine; the artifact generation is not yet complete.

The Extraction Process

The key idea is that these are not separate programs. They are views of the same system.

Spine's validated AST provides a unified structure from which different verification targets can be projected.

Logical constraints project to Z3 queries. Temporal declarations project to TLA+ specifications. Behavioral and process declarations project to mCRL2 specifications.

Each projection preserves the relevant structure from the original program. The compiler handles the translation. The developer works in one language.

Verification and Universes

In the previous post, we introduced universes as structured context.

Verification depends on which universe the system operates in.

An invariant might hold universally in the general system, but require additional conditions in a specific jurisdiction. A temporal property might be satisfied under one set of rules but violated when organization-specific policies are added.

Because universes are explicit, the compiler can generate verification targets for each context. This means we can ask not only "does this property hold?" but "does this property hold in this universe?"

Verification and Resources

Resource tracking interacts with verification in a useful way.

Many invariants that would normally require proof become structural consequences of linearity. If ownership is linear, uniqueness is guaranteed by the type system — not by a verification pass.

This means the verification pipeline can focus on the properties that cannot be established by resource discipline alone: liveness properties, temporal ordering, probabilistic bounds, process equivalence, spatial invariants, and cross-universe consistency.

Resource tracking and verification are complementary. One handles structural guarantees. The other handles behavioral ones.

From Local Checks to Global Reasoning

Traditional testing asks: "Does this function produce the right output for these inputs?"

Verification asks something stronger:

These are not questions about individual executions. They are questions about the system itself — its entire space of possible behaviors.

Because Spine makes facts, rules, effects, and invariants explicit, these questions become answerable as part of ordinary development.

What This Does Not Replace

Verification is not a silver bullet.

It cannot check properties that have not been stated. It cannot verify interactions with external systems that are not modeled. And for some properties, the state space may be too large for exhaustive checking.

But it can catch entire classes of errors that testing misses — errors that arise from unexpected combinations of valid actions, subtle interactions between rules, or edge cases in temporal behavior.

The goal is not to replace testing. It is to provide a fundamentally different level of assurance for the properties that matter most.

A Subtle Shift

With verification integrated into compilation, the relationship between writing code and reasoning about correctness changes.

You do not write a program and then separately try to verify it. You describe a system — and the act of description carries verification with it.

This is where everything we have built comes together: facts give structure to check, invariants give properties to verify, effects give transitions to explore, processes give concurrent behavior to analyze, spatial structure gives containment and locality to reason about, resources give structural guarantees, and universes give context to verify within.

Looking Ahead

We have described systems and verified them. What remains is the question of how they become executable.

In the next post, we will follow a Spine program from surface syntax through its intermediate representation to compiled machine code — the compilation pipeline that turns structured descriptions into efficient, running programs.

← Previous: Universes as Context Next: From Spine to Machine Code →