Glossary

The series glossary.

The entries below are the series glossary for Trust and Proof, Goal-Relative Assurance, and Agentic Process Governance. The same term has the same sense in all three papers. Where a later paper applies a term from Trust and Proof to a generated execution, the entry says so. Each entry states that sense and adds nothing to the claims.

Relations and predicates

Trust
A relational attitude toward an agent, institution, method, or machine. It is not an evidentiary object. (Trust and Proof.)
Proof
An inspectable evidentiary object supporting a proposition: a formal derivation, cryptographic proof, certificate, or test result. Used more broadly than a derivation in a fixed formal system. (Trust and Proof.)
T(x)
Provisional predicate: x is trusted. Used only to state the opening claims. It does not survive as the working notation. (Trust and Proof.)
P(x)
Provisional predicate: x is proved, with the boundary left implicit. The working form is P(x | A). (Trust and Proof.)
𝒯, 𝒫
The set of trusted things and the set of proved things. Equivalence of the opening claims is 𝒯 = 𝒫. The two necessity claims are the inclusions 𝒯 ⊆ 𝒫 and 𝒫 ⊆ 𝒯. (Trust and Proof.)
Equivalence
The claim ∀x, T(x) ↔ P(x), or 𝒯 = 𝒫. Both necessity arrows taken together. Refused as a description. (Trust and Proof.)
Necessity
The question which of T(x) → P(x) and P(x) → T(x) holds, if either. Each universal arrow is refused as a description. (Trust and Proof.)
Substitution
The claim that proof can stand in for a demand for trust. The coarse form is P(x) → ¬Need(T, x). The form that can hold is the local one below. (Trust and Proof.)
P(x | A)
The required property of x is established relative to a set A of assumptions and dependencies. This is the shape of a proof claim, not a caveat attached afterwards. (Trust and Proof.)
Need(T, x | A)
Given A, acceptance of x still requires trust in x. Replaces the provisional Need(T, x). (Trust and Proof.)
P(G_a, x_i | A_g^i)
The goal-relative proof: execution x_i satisfies governing goal G_a relative to the proof-support set. The goal is in the property place. The execution is an argument, not a member of the support. This is the proof inside discharge.
P(G_a, x_i | A_i)
The same goal and execution, relative to the execution boundary. Agentic Process Governance calls this the governed claim. Hygiene does not make it the same formula as P(G_a, x_i | A_g^i).

Boundaries and residue

Proof boundary
The set in the conditioning place of a proof claim: A in Trust and Proof, A_g^i for the proof inside discharge, and A_i for the governed claim P(G_a, x_i | A_i). Individuated at the level of atomic trust requirements. A “one-of-n honest” or “k-of-n honest” condition is one member, not n members. Acyclic discharge is assumed, so the residue is a flat set; circular discharge would need a family of minimal trusted sets.
Trust residue R(A)
R(A) = {a ∈ A : Need(T, a | A ∖ {a})}. The part of the boundary that still has to be trusted once the rest is granted. The set difference is ∖ in all three papers.
Local trust discharge
P(x | A) → ¬Need(T, x | A). The proof removes the demand to trust the subject x itself, given the boundary. The later papers keep this formula for that subject. They do not restate it for x_i, because the execution is not a member of A_g^i.
Global trust elimination
R(A) = ∅. Nothing in the boundary is left to trust. Not entailed by local discharge. None of the papers requires the residue to be empty, and none treats emptiness as implied by a valid proof.
Trust Displacement Result
P(x | A) ∧ ¬Need(T, x | A) ⇏ R(A) = ∅. A proof may discharge trust in x and still leave a non-empty residue. Where the execution is not a member of the support, the same result is P(G_a, x_i | A_g^i) ⇏ R(A_g^i) = ∅.
Trust-dominates, ≺ₜ
Written on the boundaries being compared. A₂ ≺ₜ A₁ when R(A₂) ⊊ R(A₁), and A_g^j ≺ₜ A_g^i when R(A_g^j) ⊊ R(A_g^i). The relation compares residues. It does not require the boundaries themselves to be nested. It is a strict partial order over a shared universe of assumptions. “More trustless” means a strictly smaller residue, not the absence of trust. Cardinality is not the measure. Incomparable residues are residue migration, not a failure of the order.
Incomplete engineering claim
A proof claim that does not expose its material A. (Trust and Proof.)
Governance (boundary management)
Naming the proof boundary, discharging what can be discharged, and remaining answerable for its residue, including when that boundary changes while the visible action does not. Not a second proof of the subject, and not the accumulation of logs or proof objects. Agentic Process Governance keeps that work and requires the goal, the local obligations, the trace, the execution boundary, the proof-support set, and the residue to stay visible together.

Goal, support, and floor

Governing goal G_a
What must be true for cases of type a. Instance formulas use G_a, not a bare G. At system time t the goal is G_a(t). The time argument is a function, not a subscript, so t is not a case type.
Execution x, x_i
What the system actually did. In Agentic Process Governance, x_i is the append-only trace of actions the gate has allowed, with their parameters and results. A denial is recorded and does not advance the state the next proposal is judged against.
Actual execution boundary A_i
The material assumptions and dependencies introduced or relied upon by execution i. Wider than the proof-support set. (Goal-Relative Assurance; Agentic Process Governance.)
Mandatory goal-assurance floor A_G
The assurance requirements imposed by the governing definition of G, required of every acceptable proof of that goal. Requirements, not the concrete mechanisms that satisfy them. A change to A_G is a governance event, not an execution decision. Use. Goal-Relative Assurance says R(A_G) should not be read as a residue in the same sense as R(A_g^i).
Instance-specific proof-support set A_g^i
A candidate set of concrete assumptions and dependencies used as the boundary of the proof claim for instance i. Not defined as the unique sufficient set, and not defined by minimality. Sufficiency for the proof is P(G_a, x_i | A_g^i). Sufficiency for the governing purpose also requires covering.
S_i, E_i
A_g^i = S_i ∪ E_i, where S_i instantiates the mandatory floor and E_i holds assumptions introduced by the facts of instance i. (Goal-Relative Assurance.)
Covering, ⊨
A_g^i ⊨ A_G when every requirement in A_G is instantiated by some assumption in A_g^i. Satisfaction in substance, not membership of a requirement’s name in the support. Requirements and assumptions are different types. Independent of P.
Boundary hygiene
A_g^i ⊆ A_i. The support used sits inside the execution boundary. Required for discharge. Not a theorem of P or of ⊨. When it holds, the support is typically a proper subset, A_g^i ⊂ A_i.
Boundary Sufficiency
A_g^i ⊨ A_G ∧ P(G_a, x_i | A_g^i). Necessary for discharge. Not discharge. (Goal-Relative Assurance.)
BS(G_a, x_i, t)
Boundary Sufficiency evaluated at the point of consequential discharge at time t. (Goal-Relative Assurance.)
Goal authority
The authority that fixes A_G and the covering, outside the execution whose validity it constrains. (Goal-Relative Assurance.)
Execution autonomy
The freedom to choose x_i and A_g^i. It does not include choosing the floor, the covering, or defining the floor from the support just built. (Goal-Relative Assurance.)
Execution residue R(A_i)
The trust residue of the execution boundary. (Goal-Relative Assurance.)
Goal-relative residue R(A_g^i)
The trust residue of the proof-support set. The residue discharge is concerned with. Inclusion of supports does not yield inclusion of residues: A_g^i ⊆ A_i does not imply R(A_g^i) ⊆ R(A_i). What does follow, when hygiene holds, is R(A_g^i) ⊆ A_g^i ⊆ A_i.
Endogenous boundary
A proof boundary partly constructed by the execution that will later be accepted against it. A run is a finite sequence A_i^0 → x_i^1 → A_i^1 → … → A_i^n. (Goal-Relative Assurance.)
Execution time τ
Time within one execution, during which the agent may construct and modify its boundary. (Goal-Relative Assurance.)
System time t
Time across successive executions, model versions, policy versions, and regulatory regimes. Written as a function argument: A_G(t), x_i(t), A_g^i(t), A_i(t). A_G(t) need not equal A_G(t+1). Equality of traces does not force equality of boundaries or of residues. t is not written as a superscript. (Goal-Relative Assurance.)
Process identity
The invariant that every valid execution is the same process. The papers replace it with goal satisfaction. (Goal-Relative Assurance.)
Goal satisfaction
The invariant that every consequential execution establishes the required goal against a support that meets the independently governed floor. Distinct executions and distinct boundaries may still satisfy one G_a. (Goal-Relative Assurance.)
Procedural conformity
Assurance obtained by constraining the path. Contrasted with goal-relative proof, which permits path variation and requires each generated path to carry sufficient evidence. (Goal-Relative Assurance.)

Discharge

Discharge(G_a, x_i)
The claim that execution x_i may be accepted as having discharged governing goal G_a. Relative to the instance support, the floor, and the residue policy. Not a function of G_a and x_i alone.
Proof validity
P(G, x_i | A_g^i), or P(G_a, x_i | A_g^i). The execution establishes the goal relative to the support actually used.
Floor satisfaction
A_g^i ⊨ A_G. The support meets the mandatory floor. Agentic Process Governance also calls this the floor charge, and says it is covering, not a second floor standing beside a formalized axiom set.
Residual-trust acceptability
Acceptable_G(R(A_g^i)). The residue of the proof-support set is acceptable for this goal under the governing policy. Acceptable_G is a parameter. It is not a theorem of P, and it is not derived from the trace.
Discharge, the only-if
A sound discharge claim holds only if four conditions hold: proof validity, floor satisfaction, residual-trust acceptability, and boundary hygiene A_g^i ⊆ A_i. The first three are independent of one another. Hygiene is not part of that independence result. The converse is not claimed. Meeting the four conditions does not by itself constitute discharge. The rule does not require R(A_g^i) = ∅.

Failure modes

Boundary insufficiency
The proof is valid relative to the support it used, and that support does not meet the floor. Strong form: ∀ A_g ⊆ A_i, ¬(A_g ⊨ A_G). Weaker form: some unused A ⊆ A_i covers the floor, and the support actually used does not. (Goal-Relative Assurance.)
Silent boundary substitution
An execution appears to meet a requirement in A_G while replacing the permitted mechanism with another that does not discharge that requirement. The reason A_G is semantic rather than a list of component names. (Goal-Relative Assurance.)
Self-justifying execution
The same unconstrained decision selects the path, the evidence, the reading of the floor, and the authorisation. If A_G is defined as whatever A_g^i already covers, Boundary Sufficiency collapses to P. (Goal-Relative Assurance.)
Residue migration
An architectural change replaces one residual dependency with another, so neither residue is a proper subset of the other. The boundaries are incomparable under ≺ₜ. A scalar trust score can hide the change. (Goal-Relative Assurance.)

Agentic process

Allow
The gate’s decision to permit one consequential action before it executes. A control on that action. It becomes part of x_i. It is not, by itself, the assurance claim, and it is not discharge. (Agentic Process Governance.)
Gate
The decision, from the current state and the pinned policy, on which consequential actions would be allowed next. (Agentic Process Governance.)
Harness
The software that runs the model and submits its proposed actions to the gate. (Agentic Process Governance.)
Trace
The append-only chain of actions the gate has allowed, with their parameters and results. Monitors and human review read this chain, not the model’s unexecuted plan. Identified with x_i in Agentic Process Governance.
Policy machine
The closed alphabet of consequential actions, guarded transitions, and invariants into which the pinned policy is compiled. Every consequential action is proposed to it and allowed or denied by it. A proved property of the machine is a stronger fact than an allow, and it is not the four-part discharge. (Agentic Process Governance.)
Skill
The compilation of the same pinned policy into the form the model reads when it proposes the next actions. Proposals become part of the trace only after the machine allows them. (Agentic Process Governance.)
Double compilation
One pinned policy compiled into the policy machine and into the skill. They agree when every action the skill can propose is an action the machine can gate, and every guard the machine enforces is still visible to the skill. Stated as a design constraint in Agentic Process Governance, and not derived from the other two papers.
Local obligations
The predicates the goal depends on. A member of the proof support is not an obligation. An unresolved predicate of the goal is not, by that fact, a member of A_i. (Agentic Process Governance.)
Proof-carrying execution
An execution that carries an assurance object sufficient to reconstruct G_a, A_G, x_i, A_g^i, A_i, P(G_a, x_i | A_g^i), R(A_g^i), and where material R(A_i). An analogy with proof-carrying code, not a claim that proof-carrying artefacts are new. (Goal-Relative Assurance.)

Shared notation

  • P(x | A) is a required property of x relative to A. P(G_a, x_i | A_g^i) is that form with the goal in the property place. P(G_a, x_i | A_i) is the governed claim, relative to the execution boundary. The two goal-relative formulas are not the same claim.
  • A proof boundary is whatever set stands in that conditioning place. The execution boundary is always A_i. The proof-support set is always A_g^i.
  • The residue uses ∖. Trust-dominance is written on the boundaries and defined by proper inclusion of residues. It does not require the boundaries to be nested.
  • Discharge has four conditions. The first three are independent. Hygiene is the fourth. Meeting the four does not by itself constitute discharge.
  • Local trust discharge is P(x | A) → ¬Need(T, x | A). The goal-relative restatement is P(G_a, x_i | A_g^i) ⇏ R(A_g^i) = ∅, because x_i is not a member of the support.
  • i and j are instances. τ is time inside one run. t is system time and is written as a function argument, as in G_a(t) and A_g^i(t).

One further entry

Peras
(πέρας). The classical word for a limit: the boundary that makes a claim definite. In this work the limit is what was shown, given which assumptions, and what is still trusted. The English for it is “limit”.

Terms the series list does not enter

These stay because Agentic Process Governance gives them a fixed sense. They do not replace an entry above. Residue comparison is the trust-dominates relation. A local obligation is the entry under that name.

Conjunction, branch, dependency
The three ways obligations compose: a final conjunction joins otherwise independent obligations; a branch chooses among alternative structures; a dependency orders one obligation after another. Without a dependency, no single order is prescribed. (Agentic Process Governance, §6.)
Agreement on a shared fact
That two local proofs restrict to the same value (for example, the same income figure) inside one boundary A_i. The maps that would establish this are not defined in the paper; it is left open. (Agentic Process Governance, §7.)
Selection rule
The rule that would choose between two incomparable proof-supports that both cover the floor. Owned with the floor; not supplied by the paper. (Agentic Process Governance, §4, §7.)

Terms used on the site

These terms stay because the site already uses them. They do not replace a sense above.

Agentic AI
Software that takes actions in your systems, not only text answers.
An agentic AI can book a trade, update a record, release a payment, or change a supplier’s status. It does not only summarise a document.
Deterministic
The same inputs always produce the same allow or deny.
If the system state and the proposed action are the same, the outcome is the same every time.
Deterministic governance
The same gate, described for a reader who starts from the decision.
The AI proposes an action. A validator decides. The same state and the same action always get the same verdict. This is the same gate as proof-gated architecture, not a second framework.
Probabilistic
Right most of the time, and not every time.
A large language model may follow a rule almost always, and still break it. That can be acceptable for a draft. It is not enforcement when a rule must hold.
Validator
The component that decides whether an action is allowed.
The Compliance Operator is the gate. Anchor is a pattern used with it. Proof Fabric is that pairing, not a second product.
Invariant
A rule about your system that must always be true.
For example, no client may own more than 10% of any fund. Spec++ is the method for writing that rule so a machine can check it.
Formal specification
A precise description of how a system may behave, written so a machine can check it.
It describes states, events, and rules. A tool can then check properties of every behaviour the specification allows, not only the cases in a test.
State machine
A workflow modelled as states, and as the moves allowed between them.
A payment request might move from draft, to approved, to released. In the Compliance Operator, each move is governed by an explicit rule, so a forbidden jump does not happen.
Spec++
The method for writing a policy so the gate can be proved.
Spec++ is how a policy is written so it can be checked and enforced. It is ready to use in a customer engagement. It is not a product.
Specification-driven development
How the software engagement is done with your engineers.
Specification-driven development is the way we write and keep the policy with your engineers. It is not a contact interest, and it is not a separate offer.
Compliance Operator
The only current product.
A formally consistent policy and a maths-proved gate. In the software that runs the model, it is the plugin that allows or blocks a tool call before the tool runs. CECO is that product, not a product family.
CECO
The same product as the Compliance Operator.
CECO is the short name, once you have seen Compliance Operator. Anchor is not a chain-layer product beside it.
Policy-constrained authorisation
An action is allowed only when the stated policy passes.
Every consequential action is checked against the policy before it runs. Permission to call an interface is not enough. The record has to show which policy applied, and that it held at decision time.
PCAS
A policy-constrained authorisation system: a formal model of who may do what, and when.
It describes the rules for accepting or rejecting an action in a state machine, with proofs that those rules hold. The Compliance Operator implements this pattern. The AI is not the authorisation layer.
Proof-gated enforcement
Evidence that the gate ran against the stated policy.
The record shows that a consequential action was checked against the stated policy, and that the gate’s verdict was honoured before the action took effect. The record is evidence the gate ran. It is not a claim an examiner has accepted. See the gate.
Proof Fabric
The Compliance Operator and Anchor used together.
The gate decides. Anchor is a researched and prototyped pattern: a portable receipt of what was allowed. Proof Fabric is that pairing. Previously called the Trust Fabric. It is not a product. See Proof Fabric.
Anchor
A researched and prototyped pattern: a portable receipt.
Data stays off-chain, in each owner’s own store. You reach Anchor through the Lean-proved software offer, not as a product card. See Proof Fabric.
Trust passport
The receipt: hashes, outcomes, and time. Not the book.
A compact record that a rule held, at a stated time, including when the answer is no. Terms and certificates stay off-chain. The trust passport is a receipt, not a product.
Zero-knowledge proof
A way to show that something is true without revealing the underlying data.
You can show that a check passed without exposing the client data the check used.
Hash-chained audit log
A log in which each new entry locks the entries before it.
Each record contains a fingerprint of the one before it. If someone changes a past decision, the fingerprints stop matching.
Neuro-symbolic agents
Agents that combine learned behaviour with rules a machine can check.
The learned part proposes. The checkable part is the rule. The term is a definition. It is not a research programme on this site.

For how a policy is written so the gate can be proved, see the Spec++ method.