unpingable

James Beck

The design and assurance layer operations never had.

Unpingable is a self-hosted platform for governing how operational observations become claims, decisions, and actions. The constellation running today is the assurance kernel: it decides what may be relied on, what may act, and what must refuse — and leaves a receipt either way.

Systems routinely skip the steps. An observation becomes a claim, a claim becomes a permission, a permission becomes an action — without the conversions being made explicit, and without re-checking that they still hold at the moment they are used. A credential valid at check time is spent after it expired. A monitor that was green authorizes a change. “Tests passed” becomes “safe to apply.” Each was true earlier; by the moment of action it is stale, unsupported, or out of scope.

The components are small and self-hosted, but they are not a pile of policy middleware — they implement one shared model of what must hold before action. Automation may propose work: runbooks, scripts, Terraform plans, AI agents. It cannot approve its own output, spend permission that has expired, or turn a demonstration into an operational fact. Every decision, and especially every refusal, leaves a verifiable receipt, not a log line.

Those conversions belong to a designed operational system — and that design is the layer still missing. It lives today in doctrine and in the operator’s head, not in an artifact the tools can read. Naming it is the design layer below: a candidate, not a shipped tool.

The same failure shows up across domains — operations, AI agents, distributed systems, formal verification, governance. Not separate programs; each is a place the one problem appears. Internally the invariant is evidence custody: deciding whether a claim may become an operational premise. Small self-hosted tools; proof artifacts on the side.

contractAgents may propose work; gates decide whether the proposal is admissible; operators decide whether governed output is promoted.

not approvalAn agent saying “done,” tests passing, a completed run, a green check, or a demo.

evidenceEvery refusal names the gate, the failed predicate, the clock basis, and whether any effect occurred.

Start with the incident: valid at check, refused at action →

Where to start — the same problem, five environments

Operations / SREThe incident write-up — a check-then-act race in postmortem form — then run the demo.
AI agentsagent_governor and wicket — typed proposals in, gate verdicts and refusal receipts out.
Formal methodsThe Lean proof reader’s portal — refusal-class boundaries, machine-checked.
PublicationsThe research index below, or the papers repo.
BackgroundWhy a lab and not a product, and what it is and isn’t — about. Reference: limits, glossary, components.

The design layer candidate

The tools do not operate over “the enterprise.” They operate over a system someone composed on purpose — its boundaries, identities, relationships, and the evidence that would count for each. That composition is real, and it is currently unwritten: it lives in doctrine and in the operator’s head. Every tool below re-derives it by hand.

Writing it down is the missing layer. An authored, versioned design; validated and ratified rather than silently amended; compiled into the bounded view each tool is competent to consume; then compared against what was actually witnessed. The verbs already exist across the constellation. The noun does not.

system designauthored, not discovered
ratified revisionimmutable; drafts do not govern
consumer projectionsbounded view per tool
shipped below this line
witnessed realizationnq · porter · verifier
admission / refusal / governed actionagent_governor · wicket · standing

What it would buy: a declared surface to name (“the public edge”) instead of a list of hostnames pasted between tools; a comparison of declared structure against admissible observation, where divergence is a finding rather than a silent widening; and authority that binds to an exact design revision, so a changed system does not inherit the old permission.

One narrow case already runs

A firewall rule is a small declaration: this traffic is refused. nq can read that rule over a read-only connection and probe the path from a named vantage point — and then refuse to let the declaration and the observation be quietly merged into one story. It is not a firewall test. nq never rules the firewall correct or broken; it holds the two apart and says which one it actually saw.

The discipline is in what it will not say. A rule that does not match is cannot testify, never “allowed.” A blocked path proves nothing by itself — a dead vantage point looks exactly like a working rule — so “blocked” is only admissible alongside a control probe to a known-reachable target proving the vantage had a way out at all. Only a real completed handshake to a declared-denied address is an unambiguous contradiction; a rejection packet is not a way through. The verdicts are typed and there is no is_ok() — a test asserts the receipt contains no healthy and no green.

Pointed at a real firewall — a blocklist rule with 17,007 entries behind it — the answer was cannot testify: the rule was present and readable, the vantage had ordinary egress, and the path itself was deliberately never probed, because probing it means firing a packet at a named malicious host to make a demo look better. The verdicts that would be interesting exist only on a scratch firewall built for the purpose, and the got-through case had to be staged with a deliberately broken rule. nq has never caught a real firewall failing to enforce a real block. It has shown it would notice.

Status: named, not ratified. No implementation, no schema, no wire format — the filing is a handle for review, not authorization to build. It is on this page because the recognition is real and the site records direction honestly, not because anything ships. The firewall probe is one rule at a time, with none of the design layer above it: evidence the comparison is worth generalizing, not evidence that it exists. Nothing above the line is built.

The assurance and custody kernel

The layer that does exist, in parts. The edges are the product; the components implement them.

Not a policy engine. Not a hosted platform. Not an AI-safety oracle.

Assurance and custody kernel. Five domains — observation, claim, premise, action, evidence — with the conversions that must be earned between them; three side obligations: retraction, capacity, seal; and one candidate layer upstream: system design. observation claim premise action evidence nq wicket standing agent_ governor system design retraction capacity seal

Select an edge for the claim it enforces. Solid shipped; dashed mapped, not built — including the design layer upstream. Drill runs demonstrate structure — they cannot confer operational effect.

Components — what each handles, and what it refuses

Python libraries and CLIs you self-host. nq is one binary; verifier ships a Z3 sidecar; Lean is for proof artifacts (read-only audit, not runtime). No SaaS, no hosted control plane. Badges: operational in daily use · research exploratory.

nqoperational
handles
observation→claim preflight for operational systems
refuses
assertion that abandons its evidence
proof
SQL-interrogable evidence store; every claim traceable to its observation
inquiry
Ask a question with a budget attached. You write the question down first — which targets, what limits, what deadline, and, up front, what this question cannot answer. Then reading is spending: attempts are counted and capped before the first DNS lookup, and a failed attempt still costs. In the worked certificate example the entire authorized budget is four work units and 750 milliseconds. The answer comes back sealed, with the evidence, the spend, and the refusals attached — and what it found cannot fund whatever you ask next.
wicketoperational
handles
premise preflight for agentic intents
refuses
intents from revoked or out-of-scope actors
proof
spec harness; typed preflight verdicts
standingoperational
handles
permission and entitlement observation
refuses
attesting permission it cannot verify
proof
permission receipts with observation age
nightshiftspecimen
handles
deferred governed work
refuses
completion claims without reconciliation
proof
work receipts; reconciliation trail
agent_governoralpha
handles
sits between an AI coding agent and its keyboard. Every action — writing a file, running a command — asks first. You approve, deny, or let read-only stuff through.
refuses
agent saying “done” treated as operator approving; tests passing treated as code ready to land; a rehearsal treated as production; permissions used after they expired
proof
golden refusal corpus; content-addressed receipts; Lean-audited class boundaries
receipt
dda5a1e5… — permission valid at check, expired at action, gap on a named clock. Reproduce: demo/refused-spend.sh
continuityoperational
handles
governed state persistence across sessions
refuses
state mutation without a receipt
proof
hash-chained receipts
verifieroperational
handles
formal constraint checks (Z3 sidecar)
refuses
proposals that violate declared constraints — specimen: the stale-standing denial
proof
examples/stale-standing-denied.json + golden output pinned to the README

Projects

Outside the core stack: supervised runs, field labs, and one-off experiments. Core components are listed above.

Supervised runs

Where you supervise an AI coding agent through agent_governor.

maude Executor desk for governed agent runs. Plans are authored elsewhere; maude takes a bounded plan, launches the coding agent as a supervised process under agent_governor, and puts every action through the gate. An approved run binds a lease — the write paths and commands it may use, and when that expires — so the run proceeds without asking about every keystroke. Maude mints no authority of its own. At the end, review the diff and promote it or throw it out.

Field lab — ATProto / Bluesky

A live network where custody, receipt, drift, and moderation claims get stress-tested in public. Not the core stack; the place the core stack meets weather.

rpp Receipts and reviewability overlay for ATProto.
atproto-labelwatch Monitor labeling activity across the network, flag integrity-risk patterns. Live →
atproto-driftwatch Track how claims propagate and mutate. A labeler that doesn't emit labels.
atproto-labeler Custom labeling service with governed drift detection.
atproto-feeds Source-first signal desk. Structural feed ranking that rewards originality over engagement. Live →
atproto-archive Personal corpus archiver into JSONL and plaintext.
atproto-stats Follow noise analyzer. Interaction density, posting cadence, graph statistics.

Other

grid-dependency-atlas Interactive map of communities exposed to infrastructure decisions made outside their control. Explore →
lexidoku Wordle meets Sudoku. Every row is a word, every column is a word. Local certainty causing global misery. Play →

Research

The papers name the failure classes; the tools above carry the response. The Δt series is scaffolding for the check-vs-action logic in standing and agent_governor. Some of this work is theoretical only; not everything here has an instantiation yet.

Selected papers below — full list in the papers repo.

Temporal Coherence & Δt Theory

Selected claims from this series are formally audited in Lean — see unpingable/lean (proof reader’s portal).

Systems & Institutional Dynamics

Alignment & Reward Dynamics

Governance & Epistemic Architecture

Papers repo