OpenVerifiers · Open source · Python

Never trust agents blindly again.

A toolkit for verifying AI agent claims — plans, derivations, factual assertions — with explicit, checkable evidence. Not a scoring layer: a proof path you can walk.

PackagingPython SDKCLIMCP server

The problem

Confidence is not evidence.

LLM output sounds right far more often than it is right. A generated plan can look coherent while silently contradicting itself, dropping a stated constraint, or asserting facts that don't follow from the evidence given.

What most agents return

“Here is your plan. It should work.”

* no proof of coherence
* no evidence for the assertions
* contradictions silently absorbed

What OpenVerifiers returns:

SAT — every constraint checked, every step derived.
UNSAT — the minimal set of conflicting facts, explained.
UNKNOWN — why it can't be proven, and what would settle it.

Architecture

Two pipelines. One evidence trace.

Claims that reduce to formal logic get checked by solvers. Everything else gets judged with calibrated confidence. Both routes write into the same trace.

Symbolic pipeline

core shipped

Deterministic, solver-backed.

Claims are translated into formal constraints and resolved by solvers — sympy for algebra, Z3 for satisfiability. A failure returns the minimal conflicting set (an unsat core) rendered as a human-readable chain, not a pass/fail flag.

  • dimension check — every rule precondition
  • sympy.algebra — symbolic resolution · shipped
  • z3.sat — constraint solving · in progress

Statistical pipeline

in progress

Judge, calibrated.

For claims that don't reduce to formal logic — qualitative or semantic judgments — an LLM-as-judge layer returns a calibrated confidence score with rationale, never a bare verdict. Deliberately sequenced after the deterministic core.

  • confidence score — not a verdict
  • known failure modes — surfaced, not hidden
  • same trace — one evidence store for both

The proof graph

A proof you can walk.

Facts and rules live in one DAG — no loops, ever, enforced by construction. The same structure runs both ways: induction derives forward from known truths, deduction decomposes the target back to knowns. This is a real trace from the physics slice.

proof trace · physics slice · real engine output

u · initial velocity0 m/sa · acceleration2 m/s²t · elapsed time4 sv = u + a·tkinematics.v_u_atrulev · final velocity8 m/sm · mass5 kgK = ½·m·v²energy.KE_half_mv2ruleK · kinetic energy160 J
givenderivedtargetrule

Induction — derive forward from known truths until the target is reached.

Trace-back

Why it failed, not just that it failed.

The same structure that derives answers explains failures. Every rejected branch, dead end, and join stays in the trace — and the conflicting facts get surfaced. This is a real failing run: kinetic energy asked for, mass never given.

failure trail · a claim that cannot be proven

K · kinetic energytargetK = ½·m·v²energy.KE_half_mv2rulem · massmissing givenK stays unknownverdict · NOT a failure state
  1. 01derive — find a rule that produces K (kinetic energy)
  2. 02candidate · energy.KE_half_mv2 — precondition: needs mass (m)
  3. 03deadend · mass — no rule or known fact produces m
  4. 04deadend · mass — needed for rule dynamics.F_ma
  5. 05REJECT (recursion) — circular: kind mass already on path
  6. 06UNKNOWN · K — no rule could derive the target from available givens
  7. 07evidence needed — a mass value, or a rule that produces one

The one cause

Every rejected branch points at the same gap: mass. K = ½·m·v² needs it, no rule or given produces it — so the engine returns an explained unknown, not a false pass or an opaque error. Add one fact, re-run, done.

Unknown is first-class

"Can't prove it" is a verdict —
not a failure state.

When the givens can't reach the target, the system says so — and why, and what evidence would settle it. Downstream consumers can distinguish “proven wrong” from “not yet provable” instead of inheriting false certainty.

Core data model

Facts, rules, and unknowns.

Three node kinds. Typed. Recursive. Everything references its derivation.

Fact node

id, value, typed attributes (domain-specific types included), a source, and a derivation reference. Facts can contain sub-facts recursively — a car decomposes into chassis, engine, and so on.

truthunverified_truthderivedtargetunknownestimated (planned)

Rule node

A precondition (dimension/type matching must hold before the rule fires), a relation — the actual math or logic — and a solver hook that resolves it. Rules are domain-defined but engine-agnostic.

precondition · dim(a) = L·T⁻²

relation · v = u + a·t

solver · sympy.algebra | z3.sat

Unknown node

A first-class outcome that carries why it is unknown and what evidence would resolve it — modeled as acknowledged unexplained, never silently erroring.

reason · no rule or given produces m

evidence · add missing given or rule

status · unknown ≠ UNSAT ≠ error

MCP integration

Plug it into any agent.

Any MCP-speaking agent calls verify() as a tool — plans get checked before they execute, claims get evidence before they travel. Transport is in progress; the SDK boundary is already clean for it.

// any agent, any framework

openverifiers serve --mcp

// now a tool in your agent's toolbox

verify(claim, evidence) → verdict + trace

// verdict: SAT | UNSAT | UNKNOWN

SDK and CLI work standalone today. The MCP transport layer is the in-progress wrapper — no domain logic leaks across the boundary.

Roadmap

Honest about where it stands.

Shipped, in progress, under research, and exploratory — labeled exactly. The repo is public; every item here links to real activity.
Available nowBuilt, running, benchmarked.

  • Core reasoning engine

    Induction and deduction over one fact/rule DAG — loop safety enforced by construction, memoized.

  • Typed fact model

    Five statuses, recursive sub-facts, typed attributes, sources and derivation references.

  • First-class Unknown

    Every non-verdict carries a reason and the evidence that would settle it.

  • Verbose trace store

    One store, three projections — success-path, failure-trail, full.

  • Solver core + CLI

    Dimension checking and sympy algebra behind swappable solver hooks; CLI with JSON output.

In progressDesigned, being built.

  • Physics vertical slice

    Kinematics + mechanics grammar. 20/20 problems pass the benchmark; release hardening in progress.

  • Z3 constraint hook + unsat cores

    Formal SAT/UNSAT resolution and minimal-conflict extraction over the same trace store.

  • Statistical pipeline

    LLM-as-judge with calibrated confidence scores for claims that don't reduce to formal logic.

  • MCP server

    Expose verify() as an agent-callable tool; CLI serves today, MCP transport in progress.

  • PROOF/PATH viewer

    Standalone web viewer for proof traces — design finalized.

ResearchingOpen design questions — briefs in the repo.

  • Grammar formalization

    Frame-based KR, RDF/OWL ABox/TBox patterns, property graphs — research briefs and synthesis published.

  • Correlation-chain validity

    Path analysis and SEM instead of silent coefficient chaining across proportional links.

  • Probabilistic facts

    Bayesian-network-style factorization for estimated values with confidence intervals.

  • Proof DSL + constrained decoding

    A compact domain language for proof representation; open question, not committed.

Domain expansionExploratory — nothing committed. Same fact/rule DAG; the grammar layer is the only new work.

The design record catalogs fifty domains the core model makes possible — one engine, a grammar per domain. Sequencing below is by feasibility; the physics slice is the in-progress proof of the pattern.

Next uppost-physics, highest feasibility

  • Math proof checking

    Step-by-step derivations validated against axioms and lemmas, contradiction and induction detection.

  • Code & refactor verification

    Dependency-graph consistency, no circular imports, API contract adherence between planned changes.

  • Personal goal roadmaps

    Snayu's origin domain — contradiction, dropped-constraint, and scheduling-feasibility checks.

Near-termsolid fits; sequencing not committed

  • Study-prep roadmaps

    Pacing vs. deadline, prerequisite ordering, resource and time arithmetic.

  • Travel itineraries

    Schedule-clash detection, buffer-time arithmetic, dependency chains (flight → hotel → activity).

  • Legal & contract review

    Contradictory obligations, missing preconditions, conflicting dates.

  • Financial-plan checking

    Compound interest, tax logic, and save → invest → retire dependency consistency.

STEM

  • Chemistry stoichiometry
  • Engineering design calculations
  • Statistics & data-claim checks
  • Algorithm complexity claims
  • Database migration plans
  • Circuit design verification
  • Unit conversion & dimensional analysis

Legal & compliance

  • Regulatory compliance checklists
  • ToS / privacy-policy consistency
  • Legal argument structure
  • Due-diligence document review

Finance & business

  • Startup financial-model auditing
  • Budget plan consistency
  • Invoice & billing reconciliation
  • Investment thesis consistency

Health & medical

  • Medication dosage & interaction checks
  • Fitness plan validation
  • Clinical trial protocol consistency
  • Insurance claim consistency

Personal & life

  • Habit & recurring-schedule checks
  • Career transition planning
  • Event planning logistics

Research & knowledge

  • Research-claim verification
  • Literature review consistency
  • Citation chain verification
  • Grant budget-to-scope consistency
  • Peer-review assistance

Software & AI

  • Agent task-delegation checks
  • Prompt / workflow chain consistency
  • Infrastructure-as-code verification
  • API contract verification
  • Data pipeline invariants

Government & public

  • Policy proposal consistency
  • AI-tutor supervision (flagship)
  • Public budget allocation
  • Environmental impact assessments

Creative & misc

  • Recipe / chemical-process planning
  • Game design balance
  • Architectural plan checks
  • Supply-chain logistics
  • Insurance underwriting logic
  • Personal-finance advice generation
Flagship example

Government school AI-tutor supervision

Verifying an AI teaching assistant's explanations against a fixed curriculum grammar — every answer carries an audit trail. The clearest concrete instance of a governance layer for AI in public institutions, and the easiest to explain to non-technical audiences.

The roadmap is the repo. Open issues, proposals, and design briefs live alongside the code.

Issues ↗Repository ↗

Proof, not promises.

Open source, early, and honest. Contribute the grammar, the solvers, or the open design questions.

View on GitHubOpen an issue