About

The home page has the short version. This is the longer one: what the work studies, why it is shaped this way, and where different readers should start.

The research question is general: how a system should get from an observation to an action, and what has to hold at each step. How does something seen become something believed, when does a belief become permission, and when may that permission produce a real change? The question first showed up in operations, where every day asks who changed this, how we know, whether the log can be trusted, and who approved the deploy. The same failure appears in AI agents, distributed systems, formal verification and governance. Operations is where the questions were learned, not what the work is about.

The dangerous cases happen in the gap between a check and the action that relies on it: the fact was true earlier, but it is stale, unsupported or out of scope by the time something acts on it. The software here puts small gates in that gap. Agents and automation may propose work; a gate decides whether the evidence is still good enough to act on; and every refusal leaves a record that can be inspected later.

Four kinds of object

The work sorts into four categories, and keeping them apart is most of the discipline. The program is the shared research question and the failure it keeps meeting. Artifacts are implemented systems with bounded claims that can be checked independently. Compositions are specific combinations of artifacts that have actually been run together — each one earned separately and dated, and none of them generalizing to the others. Propositions are candidate designs still under investigation: named, not settled, and usually not built.

The failure this guards against is the one every research program with more than three repositories eventually commits: presenting a set of parts as an integrated suite because they share an author and a vocabulary. Parts do not work together because they were designed to. They work together when someone runs them together and writes down what happened. The status ledger is where that gets recorded.

What this is

The tools here keep the gap between check and action visible, and make stale inputs fail before anything changes. They are small pieces: they keep what was observed apart from what was asserted, measure the time between check and action on a named clock, check an intended change before it happens, and leave records the next system can rely on. Automation proposes work — runbooks, scripts, Terraform plans, AI agents — and cannot approve itself, use permission that has gone stale, or turn “tests passed” into “safe to apply.” The whole question is whether the facts a proposal relies on were actually observed, are still current, and may be relied on at the moment of action.

What counts as approval

Approval is an explicit decision, by an operator or a gate, about one specific proposal, made at a point that carries authority and recorded with its scope, time and evidence. A completed run, passing tests, a chat message, a green check, a completed rehearsal, or an agent saying “done” is not approval. Approval is a bounded act by an operator or a gate, not a by-product of something else finishing.

Allowed is not the same as still true

Authorization asks whether an action is allowed. The harder question is whether the facts behind that action are still good enough to act on. A credential valid at check time can be stale at action time. A green check can outlive its evidence. A log line is the writer’s own report until it is sealed. A behaviour shown once in a demonstration is not an operational claim. Each of these slips is invisible to the usual tooling and cannot be recovered after the fact. Keeping them visible, and able to refuse before anything changes, is the job.

The category

The closest established analogy is electronic design automation. Not because operations resembles chip layout, but because the useful parts of EDA are compilation, checking, comparison and explicit promotion: an authored design, rule checks that refuse contradictions, compiled outputs for each downstream consumer, a deliberate sign-off step, and a comparison of intended structure against built structure in which any difference is a finding rather than a nuisance. Outwardly the category is design and assurance for operational systems; the intellectual ancestor is EDA.

This is an integration thesis, not a novelty claim. Every technique involved already exists somewhere — infrastructure-as-code declares intent, monitoring observes reality, policy engines decide, and systems engineering has modelled designs for decades. What has not happened is their integration into one discipline, with an authored description of the system as a first-class object, explicit statements of what evidence is required, a bounded view for each consumer, and typed refusals. That gap is the bet.

The analogy stays at the level of positioning and does not enter the vocabulary: nothing here is called a schematic, a netlist or a tape-out. The authored-design layer that would complete the picture is a candidate: named and designed, not built. The research directions page marks where that line falls.

Where to start

Different readers want different starting points.

• AnyoneRun the Constellation demo: an agent reports a refund done, the reply was lost, and the system records “unknown” until the provider’s own records settle it.
• Operations / SRERead the incident write-up for the check-then-act failure, then Constellation NQ for current diagnostic and evidence-evaluation paths.
• AI agentsStart with the alpha.6 walkthrough: one reviewed plan, one-use authorization, a local change carried out under a separate service’s custody, reconciliation, and a fresh read-only check. Then use the component map and integration guide to choose only the parts you need.
• How the parts combineThe Constellation front page explains the current release, the workflow that was actually qualified, and its limits. The older four-program exhibit is kept in the archive as dated history.
• Formal methodsThe Lean proof reader’s portal, where the boundaries of refusal classes are machine-checked.
• AT ProtocolATProto has received an exact shared-interface handback. Its own campaign still owns production binding, migration, notification routes, rollback and retirement of the older NQ; none of those is completed by alpha.6.
• Earlier prototypeThe incident if you read postmortems, or the descent for the artifact-rich version of the same event. Both use the deprecated predecessor.

What this is not

• Not an observability dashboard. Dashboards display claims after the fact; this work decides whether a claim may be relied on for an action in the first place.
• Not a policy-as-code replacement. Policy engines decide over the facts they are given; this work decides whether those facts may be given to them. The two combine.
• Not “AI governance” in the procurement sense. Refusals and records you can run.
• Not a hosted service. You run every part of it yourself. Alpha, solo, small on purpose — and not yet production-ready.
• Not one product suite. Shared authorship and shared vocabulary are not integration. Combinations are exercised one at a time and recorded with a date; nothing here claims that every part works with every other.
• Not a proof of safety. Lean checks the boundaries of refusal classes. Records attribute what happened in one instance. Both are narrower than “proven” — see limits.

Why a lab and not a product

The bet is that governance lives in the conversions between observation and action: what may be believed, what may be relied on, what may authorize a change, and what must stay a refusal. Ordinary infrastructure collapses those boundaries into “looks fine” in ways that only show up at incident time. A bet like that should be falsifiable, so the work ships as small tools with explicit refusal boundaries and reproducible demos.

The glossary defines the older technical terms (custody, standing, premise, witness) used on the earlier-prototype pages.