Research directions
The questions behind the software: what has to hold as evidence turns into action, and what the components are and are not yet built to answer.
This is an independent research and engineering program on preserving evidence custody as systems move from observation to action over time — formal models, executable systems, and bounded compositions. The same failure appears across operations, AI agents, distributed systems, formal verification, and governance; operations is merely where the questions were learned.
The papers name the failure classes; the software carries the response. The research catalogue lists the papers, including the Δt series that scaffolds the check-versus-action logic. Selected claims from that series are machine-audited in Lean: unpingable/lean (proof reader’s portal), and a design-constraints family that bounds specific design claims. The Δt theorems prove class boundaries of refusals — not that any deployed system is safe. See limits.
On this page: related work · the transitions under study · continuity · the authored design layer · other notes.
Related work
Haiqing Li, Xin Ma, Yinhao Wu, Wenliang Zhong, Feng Jiang, Thao M. Dang, Xiao Hu, Hehuan Ma, Yuzhi Guo and Junzhou Huang, “Who Holds the Pen? Let Specifications, Not Agents, Sign Off”, arXiv:2609.29921 (2026). Across seven models on SkillsBench, the paper measures a gap between an agent’s completion claim and the state it was asked to produce, and proposes SpecHarness, an agent harness in which a trusted runtime authorizes agent actions, observes their effects, and marks a specification obligation satisfied only from admissible, fresh evidence.
Recent work independently studies the same basic separation inside a single agent runtime: agents act, but trusted evidence determines authoritative completion. Constellation is designed for the distributed case, where the observer, authority, executor and evidence sources may be independently owned and may fail separately. That case is a design target and a roadmap: the qualified release and the demo on this site run on one host.
This is independent convergence, and evidence that the discipline is worth taking seriously. It is not validation of Constellation’s specific architecture. A longer comparison is in the literature note on agent-governance field state.
The transitions under study
Evidence does not travel from a sensor to an action in one move. It crosses a series of boundaries, and at each one something is converted into something with more force than it had a moment earlier. The recurring failure is that the conversions happen silently — nothing records that they occurred, and nothing re-checks that they still hold at the moment of use.
The table below is a schematic: it names the boundaries the program studies, not a pipeline that six named services already implement end to end. The “exercised by” column started as the July 2026 mapping onto the classic implementations (AG ng, classic NQ and the Docket Git-effect vertical); the authorization and execution rows now describe the alpha.6 state. Current components are on the components page and dated claims are in the ledger.
| Transition | The question it must answer | Exercised by |
|---|---|---|
| 1. observe → interpret | What did the instrument actually see — and what did it fail to see? A signal that disappears must become a finding, not a silent zero. | NQ — shipped, pre-1.0 |
| 2. interpret → rely | May a consumer lawfully act on this reading? Reliance is indexed to a named consumer, and a reliance refusal is never the negation of the underlying claim. | NQ reliance evaluation — shipped; consumer identity configured, not authenticated |
| 3. rely → authorize | May this exact prepared work receive authority? The decision is made over exact bytes, and the decision authority is burned once — a second issuance for the same decision refuses. | Constellation AG (formerly AG ng) — one exact composition qualified in alpha.6; not a production-deployment claim |
| 4. authorize → act | Do the authorized bytes match what is about to execute? An authenticated issuance is checked against the executor’s own stored attempt — never against the record’s own echoes — before any local standing is minted. | Docket — its frozen Git baseline admits one effect class, the atomic Git target-ref transition; alpha.6 dispatched a separate exclusive-create executor through Docket’s executor transport |
| 5. act → settle | What actually executed, and what does the surviving record establish? Settlement is a description of what occurred; it is not a safety claim, and it mints nothing downstream. | Docket settlement → NQ evaluation — exercised once; the run’s receipts are not public |
No artifact is mapped onto a transition it has not exercised. Continuity is a concern across all of the transitions, not a stage after them.
Continuity is a separate question
The last stage of a pipeline is a bad place to put memory. “Remember” is not one responsibility, and no artifact here owns it whole. It decomposes into five questions that have different owners, different expiries, and different failure modes:
- valid
- What still holds, as opposed to what merely still exists?
- attributable
- Whose testimony was it, and can it be recalled by origin?
- reusable
- May this be spent again, or was its authority consumed?
- reconstructible
- Can the decision be walked back to its premises from what survives?
- unknown
- What must stay unknown, or wait for renewed judgment, rather than be inferred?
Two of these had partial owners when this was written. Continuity holds hash-chained cross-session state, so a reliance cannot happen without a prior commit. NQ evaluates imported continuity snapshots as one narrow claim — continuity_rely_eligible — and implements none of continuity’s trajectory law. The other three are open questions, and the site does not pretend otherwise.
The authored design layer (proposition)
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 artifact 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 work. The noun does not.
| Stage | Meaning | Built? |
|---|---|---|
| system design | authored, not discovered | not built |
| ratified revision | immutable; drafts do not govern | not built |
| consumer projections | bounded view per tool | not built |
| witnessed realization | NQ · Porter · Verifier | shipped |
| admission, refusal, governed action | Constellation AG · Constellation Docket · Wicket · Constellation Standing | shipped |
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.
The one narrow case that 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 admissible only 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 that 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 demonstration look better. The interesting verdicts exist only on a scratch firewall built for the purpose, and the got-through case had to be staged with a deliberately broken rule.
Cited: the lab specimen is declared_deny_lab_subject_probe.md in the classic NQ repository. NQ has never caught a real firewall failing to enforce a real block. It has shown it would notice. That is lab-backed compatibility evidence, never live testimony about a deployed estate.
Status of the proposition: 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 that the comparison may be worth generalizing, not evidence that it exists. The first three stages in the table are not built. The ledger row carries its dated status.
Other research notes
- Governed recursive improvement — a deferred design discussion of tactics, evidence, evaluation, reserves and external amendment authority. It adds no runtime composition or release commitment.
- Staying within budget can still leave work unfinished — a bounded Lean model separating spend limits from the reserve needed to finish mandatory obligations; a formalized bridge, not an implemented controller (Lean source).
- ABSD — a small experimental operating system used partly to test these semantics below the application layer.