From Impressions to Proofs: Deterministic Verification as a Pythonic Primitive

Most agents today are scored, not verified. They produce outputs, and we evaluate those outputs with heuristics, rubrics, or LLM-as-judge pipelines. The output looks right? Score it high. It looks plausible? Trust it.

This is impression-based trust. And it breaks precisely when it matters most — when the problem is hard, the stakes are real, and the difference between correct and incorrect isn't visible on the surface.

Snayu's bet is different. We believe the future of reliable agents isn't better scoring. It's deterministic verification — extracting the grammar of correct reasoning from expert knowledge, then checking every step of an agent's derivation against that grammar instead of scoring the final impression.

This post shows how.

The PyTorch Insight: Computation Graphs as a First-Class Citizen

Before openverifiers, there was PyTorch. And before PyTorch, most deep learning frameworks treated computation as a static expression to be compiled and optimized — you declared a model, froze it, and ran it. Debugging meant inspecting intermediate tensor values. Understanding how a gradient flowed back meant reading documentation, not code.

PyTorch changed one thing: every operation became a node in a dynamic computation graph, built lazily as Python executed. .backward() didn't just compute gradients — it traversed the graph that the code itself had implicitly constructed. The graph wasn't a separate artifact you maintained alongside your code. It emerged from writing normal-looking Python.

Three properties made this work:

1. Imperative authoring, automatic tracing. You write y = w * x + b like it's algebra, and PyTorch records the operation. No separate graph definition language.
2. Typed metadata carries meaning. Tensors have shapes, dtypes, and device tags. The framework uses those tags to validate operations before execution — wrong shape? Error, not silent wrongness.
3. Interception hooks. register_hook, autograd profilers, custom backward functions — you can inspect, modify, and interrogate every step of the computation. The graph is readable.

openverifiers applies the exact same three ideas to reasoning instead of gradient computation.

# PyTorch: operations build a computation graph for differentiation
x = torch.tensor(3.0, requires_grad=True)
y = x ** 2 + 2 * x + 1
y.backward()          # traverses the implicit graph; x.grad == 8.0

# openverifiers: operations build a computation graph for verification
u = phy.autovar('10 m/s', owner=car)
a = phy.autovar('4 m/s^2', owner=car)
t = phy.autovar('10 s', owner=frame)
kin1 = phy.kinematics.newton.1().plug(u=u, a=a, t=t)
s = kin1.separate('s').evaluate()   # traverses the explicit proof graph

In PyTorch, the graph tells you how a number was computed. In openverifiers, the graph tells you why a number is true. Same structure, different semantics. Same Python, new primitive.

The Core Idea: Grammar, Not Scoring

Consider what happens when an agent tries to solve a physics problem. Today, the agent produces a solution, and we evaluate it. We might check: does the answer have the right units? Is the magnitude plausible? Does the agent's reasoning "look" correct?

This is a scoring problem. And scoring problems have a fundamental weakness: they can't prove correctness, only approximate it.

Our alternative: define the grammar of correct reasoning for a domain, then have a validator check that the agent's proof trace conforms to that grammar.

Agent output          →    Proof trace (sequence of typed steps)    →    Validator
   "s = 300 m"                        ↓                                      ↓
                              Each step references a rule,             Each step checked:
                              binds variables by dimension,            rule preconditions satisfied?
                              and produces a derivable                 dimensional consistency preserved?
                              conclusion                                 Final assertions match specs?

The grammar isn't a dictionary of allowed words. It's a set of typed, attributed rules — KCL for circuits, Newton's laws for kinematics, algebraic identities for symbolic manipulation — that specify exactly what inferences are valid from what premises. An agent that produces a derivation violating the grammar is provably wrong, not just unlikely to be right.

This shifts the engineering problem from "how do we make agents smarter?" to "how do we make verification cheap and composable?" The second question has much better tooling.

Three Problems, One DX

The proof of concept is in the code. Here are three problems at increasing complexity, all expressed in the same API — all producing verifiable proof traces.

Problem 1: Kinematics — The Basic Primitive

The simplest case establishes the core DX: typed variables with physical dimensions, relationship templates that check themselves on application, and a query language for trace verification.

import openverifiers as ov
import openverifiers.physics as phy

# Environment setup: declare objects with ownership and typed variables
frame = phy.SimpleFrame()
car = phy.SimpleObject(mass=phy.autovar('10 kg'))

with car as owner:
    u = phy.autovar('10 m/s')    # velocity, dimension [L T⁻¹]
    a = phy.autovar('4 m/s^2')   # acceleration, dimension [L T⁻²]

with frame as owner:
    t = phy.autovar('10 s')      # time, dimension [T]

# Apply a transformation template — Newton's second kinematic relation
kin1 = phy.kinematics.newton.1().plug(u=u, a=a, t=t)
s = kin1.separate('s').evaluate()

display s
# → phy.distance(value='300', unit='m')
# The computation graph records: s = u*t + ½*a*t²
# Every node carries dimensional metadata. Dimensional mismatch → error, not wrong number.

# Validator query — check the trace against a specifier
result = ov.find(1).where(owner=car, value=300, unit=phy.autounit('m'))
# → MATCH: s = 300 m, verified through 3 proof steps, all dimensionally consistent

Notice what's not here: no solver invocation, no numerical method, no "ask an LLM to compute this." The evaluate() call delegates to the logical core, which solves the constraint system and records every step. The find(...).where(...) query reads back the proof trace like SQL reads back a database — exact, typed, deterministic.

Problem 2: RC Circuit — Multi-Rule Composition

Real problems require composing multiple domain rules. KCL and KVL don't apply in isolation — they interact, and the solver must find a consistent assignment across all constraints. This is where the rule system proves its value: rules are first-class, composable objects.

import openverifiers as ov
import openverifiers.circuits as circ

# === Formal Environment Setting ===
V_source = circ.autovar('12 V', owner=power_supply)
R1       = circ.autovar('100 Ω', owner=resistor1)
R2       = circ.autovar('200 Ω', owner=resistor2)
C1       = circ.autovar('10 μF', owner=capacitor1)

I_total = circ.autovar(owner=node_a)    # unknowns
V_cap   = circ.autovar(owner=capacitor1)

# === Apply domain rules (the grammar of circuits) ===
# Each rule specifies preconditions, conclusion, and applicability

rule_kcl = circ.kcl(node=node_a).apply(
    inputs=[I_source], outputs=[I_R1, I_R2]
    # Precondition check: node_a exists, all connected branches carry current
    # Conclusion: I_source - I_R1 - I_R2 = 0 (written as a constraint node)
)

rule_kvl_1 = circ.kvl(loop=loop_1).apply(
    voltage_sources=[V_source], drops=[V_R1, V_cap]
    # Conclusion: V_source - V_R1 - V_cap = 0
)

rule_kvl_2 = circ.kvl(loop=loop_2).apply(
    voltage_sources=[V_cap], drops=[V_R2]
    # Conclusion: V_cap - V_R2 * I_R2 = 0  (Ohm's law applied within the loop)
)

# Ohm's law — a transformation rule, not a hardcoded formula
rule_ohm_1 = circ.ohms_law().apply(variable=V_R1, current=I_R1, resistance=R1)
rule_ohm_2 = circ.ohms_law().apply(variable=V_R2, current=I_R2, resistance=R2)

# === Solve the constraint system ===
system = circ.System(rules=[rule_kcl, rule_kvl_1, rule_kvl_2, rule_ohm_1, rule_ohm_2])
solution = system.solve(for_variables=[I_total, V_cap])

# === Validator assertions (what agents must prove) ===
ov.assert(I_total).value_is_known().unit_eq('A').within_tolerance(0.01)
ov.assert(V_cap).value_is_known().unit_eq('V').physically_consistent()

What changed from Problem 1: the number of rules increased, but the authoring DX did not. You didn't write a solver. You didn't configure a numerical backend. You composed typed rule objects — each with its own preconditions, conclusions, and domain applicability — and the system resolved the constraint network. The validator checks that an agent's proof of this solution follows the same rule composition path.

The critical distinction: the grammar is the rules, and the rules are inspectable objects. You can query which rules applied to a given node, trace which preconditions were satisfied by which variables, and verify that no rule was applied outside its domain.

Problem 3: Common Root of Quadratics — Deductive Proof

This is the hardest case, and the one that defines what openverifiers is actually for: mathematical theorem proving where the derivation structure matters, not just the final result.

Z3 and other SMT solvers can verify that (aq - bp)² = (bp - cq)(cq - ar) is a logical consequence of the premise that two quadratics share a root. But Z3 cannot produce the derivation — the step-by-step algebraic reasoning that a mathematician would write on a whiteboard. It can confirm the theorem is true; it cannot show you how it knows.

openverifiers' logical core does both: it verifies correctness and produces a human-readable proof trace.

import openverifiers as ov
import openverifiers.algebra as alg

# === Formal Environment Setting ===
# Two quadratics with variable coefficients
p, q, r = alg.autovars('p q r', owner=coefficients_f)
a, b, c = alg.autovars('a b c', owner=coefficients_g)
x₀      = alg.autovar('x₀', owner=common_root)

# Define the polynomials
f = alg.polynomial(coeffs=[p, q, r], variable='x')
g = alg.polynomial(coeffs=[a, b, c], variable='x')

# === The proof: step-by-step deductive reasoning ===
proof = alg.Proof(environment={
    'assumptions': [
        f.is_degree(2), g.is_degree(2),
        f.evaluate(x=x₀) == 0,          # x₀ is a root of f
        g.evaluate(x=x₀) == 0,          # x₀ is a root of g
    ],
    'targets': [
        'derive_condition_for_common_root',
        'solve_for_common_root_expression',
    ]
})

# Step 1: Eliminate x₀² by cross-multiplication
step1 = proof.eliminate(variable=x₀, from_eqs=[f, g], strategy='multiply_subtract')
# Produces: (a*q - b*p) * x₀ = c*p - a*r

# Step 2: Eliminate x₀ again using the linear relation
step2 = proof.eliminate(variable=x₀, from_eqs=[step1, f], strategy='substitute_then_factor')
# Produces: (a*q - b*p)² = (b*p - c*q)(c*q - a*r)
# ← This is the condition for a common root

# Step 3: Solve for x₀
step3 = proof.solve_for(x₀, from_eqs=[step1])
# Produces: x₀ = (c*p - a*r) / (a*q - b*p)

# === Validation ===
ov.assert(step2.conclusion).matches_formula(
    lhs='(aq - bp)²', rhs='(bp - cq)(cq - ar)'
)
ov.assert(step3.conclusion).is_expr_in_terms_of(['p','q','r','a','b','c'])

# The proof trace is now a verifiable object:
# Each step references an algebraic rule (eliminate, factor, substitute)
# Each step carries a justification string and a dependency chain
# The validator can replay every step and confirm the derivation

This is fundamentally different from what a SAT solver provides. The logical core maintains a theorem state — a database of facts, lemmas, and intermediate derivations that persist across proof steps. It applies structural reasoning: not just "is this equation satisfiable?" but "what algebraic operation transforms this equation into that one, and is that operation valid given the current context?"

The grammar here isn't KCL or Newton's laws. It's the rules of algebraic deduction: factoring, substitution, cross-multiplication, elimination. These are themselves typed, attributed rules — part of the same system as the circuit laws, just in a different domain.

Architecture: Three Layers, One Promise

The system is structured in three layers, each with a single responsibility:

┌─────────────────────────────────────────────────────────┐
│  PYTHON SURFACE                                           │
│  User writes natural Python with typed autovars.         │
│  The computation graph is the proof trace by default.    │
├─────────────────────────────────────────────────────────┤
│  openverifiers LIBRARY                                    │
│  Domain objects (frames, objects, polynomials).           │
│  Rule templates (KCL, KVL, Newton, algebraic identities).│
│  Proof construction, trace validation, query interface.  │
├─────────────────────────────────────────────────────────┤
│  LOGICAL CORE (Rust)                                      │
│  Multi-step deduction beyond SAT.                         │
│  Theorem state management.                                │
│  Rule matching and application.                           │
│  Exposed to Python via PyO3.                              │
└─────────────────────────────────────────────────────────┘

The Python layer gives you DX — writing proofs feels like writing code, because it is code. The library layer gives you composition — rules are objects that can be inspected, combined, and conditionally applied. The core layer gives you correctness — the hard deductive work happens in a language designed for it, and the Python layer only sees verified results.

This mirrors exactly how PyTorch works: the Python frontend is ergonomic, the C++ backend is efficient, and autograd sits in between connecting the two. openverifiers replaces autograd's gradient traversal with proof traversal — same concept, different primitive.

What This Enables

If the architecture holds, several things become possible:

• Agents that write proofs, not just answers. An LLM agent can construct a derivation step by step, checking each step against the grammar before proceeding. The agent isn't asked to "give the right answer" — it's asked to build a valid proof. The validator confirms or denies.

• Composable domains. KCL/KVL for circuits, Newton for kinematics, algebraic identities for mathematics — these are all rules in the same system. A thermodynamic problem that also involves circuit analysis can be expressed and verified without leaving the framework.

• Trust through structure, not scoring. A human reviewer can inspect the proof trace, read each step's justification, and independently confirm correctness. No rubric. No LLM judge. Just structure.

• The grammar itself is the knowledge base. Every rule, precondition, and theorem is an inspectable object in the system. You can query: "which rules apply to this node?", "what assumptions does this derivation depend on?", "where did this variable come from?" — and get structured, typed answers.

The Open Questions

This is still early. Several decisions will define the system's character:

1. The logical core. We're leaning toward Rust for memory safety and PyO3 bindings, but the theorem-state management and multi-step deduction algorithms are still being explored. The core needs to handle deduction patterns that SMT solvers don't natively support — structural algebraic reasoning, rule chaining with persistence, and conditional theorem derivation.

2. Proof serialization. The proof trace needs a compact, readable format for hand-authoring and inspection — beyond the Python API. We're considering a structured text format that reads like mathematical notation but serializes to typed data.

3. Rule matching strategy. Pattern-matching rewrite systems are transparent but limited. Constraint-based matching is powerful but harder to debug. The right balance hasn't been settled.

4. Dimensional analysis as a first-class layer. Every rule application should automatically check dimensional consistency before the logical core even runs. This is a cheap, high-value verification layer we're building into the rule engine directly.

The Bet

Snayu's long-term bet is that deterministic verification will become the default trust mechanism for AI-generated reasoning — not because scoring gets worse, but because the alternative — trusting impressions — doesn't scale to problems where correctness is binary and consequences are real.

Physics, mathematics, circuit design, formal logic — these are domains where the grammar of correct reasoning is well-understood, and where a wrong answer is wrong, not just unlikely. They're also domains where the gap between "the LLM produced something plausible" and "the LLM produced something correct" is the entire story.

We're building the infrastructure to close that gap — one verifiable proof step at a time.