ponens

← All specifications

Policy Specification

Version

Version: 0.2
Status: Draft
Format: Canonical typed specification with OCaml / IML-oriented DSL
Positioning: Companion specification to the Trace Specification

Changes in 0.2 (additive). Adds the residual-surface vocabulary (§15.1) — the residuals collection, residual field accessors, and the severity ordering — so policies can quantify over a trace’s declared negative space (Trace Specification §13). Adds the standard residual-surface policies (§17.4). Existing policies are unaffected.

1. Purpose

A policy is a governance formula interpreted over a trace or review case.

Policies are Computable Governance — governance you run, not a checklist or a sign-off. A policy is a machine-checkable rule, evaluated automatically over the structured trace to a pass / fail: a real gate, not a social “Approved.” This is conformance checking — the established technique behind runtime verification and declarative process mining (temporal logic over finite traces, e.g. DECLARE) — applied to the reasoning traces of AI agents.

Policies do not define execution history.
They constrain, require, forbid, or validate properties of that history.

A policy may also require a reasoner — an automated-reasoning tool (e.g. CodeLogician, ImandraX, a model checker, an SMT solver) that produces the verification artifacts a policy depends on. The optional reasoner field names one from the reasoner registry (gallery/reasoners), so a policy can demand not just that a claim was verified, but by what — the engine through which a claim becomes established rather than merely asserted.

This specification defines:

2. Relationship to the Trace Specification

This document is intended to be used together with the trace specification.

The split is:

A good one-line summary is:

Traces define the execution world; policies define the rules evaluated over that world.

More formally:

This document defines φ and the meaning of ⊨.

3. Scope

This specification currently focuses on policies interpreted over:

The core policy language is primarily designed for:

4. Design Principles

The policy system is built around six core principles:

  1. Policies are formulas, not prose
    Human-readable descriptions are helpful, but the authoritative meaning of a policy is its formula.

  2. Trace semantics are primary
    Policies are interpreted over traces; they do not redefine trace meaning.

  3. The DSL is reasoner-agnostic
    Policies should be written against semantic roles, not engine-specific artifact names or tool invocations.

  4. Temporal + structural expressiveness
    Policies must express both ordering constraints and structural / lineage constraints.

  5. Canonical typed model first
    The authoritative policy representation is a strict typed model suitable for OCaml / IML reasoning.

  6. Interchange is derived
    JSON/Pydantic projections are derived from the canonical model.

5. What a Policy Is Semantically

A policy is a well-formed formula interpreted over a trace.

Informally, a policy says things like:

Policies may constrain:

6. Canonical Policy Object Model

6.1 Policy object

type policy_severity =
  | Info
  | Warning
  | ErrorSeverity

type policy_scope =
  | TraceScope
  | ActionScope
  | ArtifactScope
  | ModuleScope

type policy_kind =
  | TraceInvariant
  | ApprovalRequirement
  | ReasoningRequirement
  | LineageRequirement
  | ReferenceIntegrity
  | ConformanceRequirement

type policy_selector =
  { action_type : string option
  ; artifact_type : string option
  ; artifact_role : string option
  ; category : string option
  ; path_matches : string option
  ; path_matches_any : string list
  }

type policy =
  { policy_id : string
  ; name : string
  ; description : string option
  ; severity : policy_severity
  ; scope : policy_scope
  ; kind : policy_kind
  ; applies_when : policy_selector option
  ; formula : policy_formula
  ; reference_artifact_id : string option
  }

6.2 Semantics of policy fields

The formula field is authoritative.
If description and formula disagree, formula wins.

7. Policy Evaluation Model

7.1 Policy evaluation object

type policy_evaluation_status =
  | Passed
  | Failed
  | UnknownEvaluation
  | NotApplicable

type policy_evaluation =
  { policy_id : string
  ; status : policy_evaluation_status
  ; checked_at_action_id : int option
  ; evidence_action_ids : int list
  ; evidence_artifact_ids : string list
  ; violating_action_ids : int list
  ; violating_artifact_ids : string list
  ; note : string option
  }

7.2 Evaluation semantics

A policy evaluation is a concrete record of checking a policy against a trace.

Evidence and violation references are supporting metadata; they are not themselves the formal semantics of the policy.

8. Satisfaction Relation

Let:

Then:

τ ⊨ φ

means:

trace τ satisfies policy formula φ

and:

τ ⊭ φ

means:

trace τ does not satisfy φ

This specification defines the syntax and intended semantics of φ.

9. DSL Overview

The policy DSL is:

This means the DSL is not merely propositional LTL.
It is a policy language over structured traces — a scoped, first-order, finite-trace temporal logic.

The foundation is deliberately well-established: LTL over finite traces (LTL_f) is the semantics behind declarative process mining (DECLARE) and runtime verification, where it has been used for conformance checking of event logs for years. This DSL extends that proven core with the predicates and quantifiers a typed trace needs — lineage, residuals (the declared negative space), and field access — so a policy can govern not just the action sequence but the trace’s structure.

10. Canonical OCaml / IML-Oriented DSL

This section defines the canonical typed representation of policy formulas.

10.1 Basic identifiers

type action_id = int
type artifact_id = string
type reference_id = string
type symbol = string
type path_pattern = string

10.2 Atomic values

type value =
  | VString of string
  | VInt of int
  | VBool of bool
  | VFloat of float

10.3 Comparison operators

type cmp_op =
  | Eq
  | Neq
  | Lt
  | Le
  | Gt
  | Ge
  | In

10.4 Temporal operators

type temporal_unary =
  | G      (* globally *)
  | F      (* finally *)
  | X      (* next *)
  | P      (* previously *)
  | H      (* historically *)
  | PTarget
  | PChain
  | HTarget
  | HChain

type temporal_binary =
  | U      (* until *)
  | S      (* since *)
  | SLast  (* since last *)

10.5 Variables

type var = string

10.6 Terms

Terms are used inside predicates and comparisons.

type term =
  | Var of var
  | Val of value
  | Field of term * string
  | Inputs of term
  | Outputs of term
  | Target of term
  | AncestorsOf of term
  | Count of set_expr
  | SetLiteral of term list

10.7 Set expressions

type set_expr =
  | TermSet of term
  | SetComprehension of
      { binder : var
      ; source : set_expr
      ; guard : policy_formula option
      ; body : term
      }

10.8 Quantifiers

type quantifier =
  | Forall
  | Exists
  | ExistsUnique

10.9 Atomic predicates

These are the semantic predicates the DSL can talk about.

type atomic_predicate =
  | ActionTypeIs of term * string
  | ActionCategoryIs of term * string
  | ArtifactTypeIs of term * string
  | ArtifactRoleIs of term * string
  | StatusIs of term * string
  | StartEvent
  | EndEvent
  | HighStakesPath of term
  | HasRationale of term
  | Completed of term
  | FailedAction of term
  | FormalModelArtifact of term
  | ApprovedReferenceArtifact of term
  | ReasoningAction of term
  | VerificationAction of term
  | StateSpaceAnalysisAction of term
  | StateSpaceAnalysisResultPred of term
  | AncestorOf of term * term
  | DerivedFrom of term * term
  | UpstreamOf of term * term
  | PredicateApp of string * term list

10.10 Policy formulas

type policy_formula =
  | True
  | False
  | Atom of atomic_predicate
  | Not of policy_formula
  | And of policy_formula list
  | Or of policy_formula list
  | Implies of policy_formula * policy_formula
  | Iff of policy_formula * policy_formula
  | Compare of term * cmp_op * term
  | Temporal1 of temporal_unary * policy_formula
  | Temporal2 of temporal_binary * policy_formula * policy_formula
  | Quantified of
      { quantifier : quantifier
      ; binder : var
      ; source : set_expr
      ; body : policy_formula
      }

This is the canonical typed DSL.
It is suitable as an OCaml representation and also naturally maps to an IML algebraic datatype.

11. IML-Oriented View

The same policy language should be representable in IML as algebraic datatypes.

A sketch of the same shape in IML-style notation would be:

type value =
  | VString of string
  | VInt of int
  | VBool of bool
  | VFloat of float

type cmp_op =
  | Eq | Neq | Lt | Le | Gt | Ge | In

type temporal_unary =
  | G | F | X | P | H | PTarget | PChain | HTarget | HChain

type temporal_binary =
  | U | S | SLast

type quantifier =
  | Forall | Exists | ExistsUnique

type term =
  | Var of string
  | Val of value
  | Field of term * string
  | Inputs of term
  | Outputs of term
  | Target of term
  | AncestorsOf of term
  | Count of set_expr
  | SetLiteral of term list

and set_expr =
  | TermSet of term
  | SetComprehension of string * set_expr * formula option * term

and atomic_predicate =
  | ActionTypeIs of term * string
  | ActionCategoryIs of term * string
  | ArtifactTypeIs of term * string
  | ArtifactRoleIs of term * string
  | StatusIs of term * string
  | StartEvent
  | EndEvent
  | HighStakesPath of term
  | HasRationale of term
  | Completed of term
  | FailedAction of term
  | FormalModelArtifact of term
  | ApprovedReferenceArtifact of term
  | ReasoningAction of term
  | VerificationAction of term
  | StateSpaceAnalysisAction of term
  | StateSpaceAnalysisResultPred of term
  | AncestorOf of term * term
  | DerivedFrom of term * term
  | UpstreamOf of term * term
  | PredicateApp of string * term list

and formula =
  | True
  | False
  | Atom of atomic_predicate
  | Not of formula
  | And of formula list
  | Or of formula list
  | Implies of formula * formula
  | Iff of formula * formula
  | Compare of term * cmp_op * term
  | Temporal1 of temporal_unary * formula
  | Temporal2 of temporal_binary * formula * formula
  | Quantified of quantifier * string * set_expr * formula

This is not meant to define the full executable evaluator here; it defines the canonical abstract syntax of the language.

12. Concrete Surface Notation

The strict typed DSL above may be rendered into a lighter textual syntax for authoring.

Examples:

12.1 Pure temporal policy

G(GitCommit -> P(RunTests /\ completed))

Meaning:

12.2 Scoped temporal policy

G(EditFile -> P_target(ReadFile \/ ReadDocumentation \/ SearchCode \/ AnalyzeCode))

Meaning:

12.3 Structural policy

G(forall input in inputs(a) -> exists! b in actions_before(a) . input in outputs(b))

Meaning:

12.4 Role-based policy

G(VerificationGoal -> target_artifact_id in {x.id | formal_model_artifact(x)})

Meaning:

13. Temporal Semantics

13.1 Future-time operators

OperatorMeaning
G φφ holds globally at every trace position
F φφ holds at some future position
X φφ holds at the next position
φ U ψφ holds until ψ holds

13.2 Past-time operators

OperatorMeaning
P φφ held at some earlier position
H φφ held at every earlier position
φ S ψφ has held since ψ last held
φ S_last ψφ held in the window since the most recent ψ

13.3 Scoped operators

These restrict the temporal search space:

14. First-Order and Structural Semantics

The DSL supports richer policies than pure propositional LTL.

14.1 Quantifiers

14.2 Set comprehensions

The DSL may derive sets such as:

14.3 Lineage predicates

The DSL may reason over:

15. Reasoner-Agnostic Vocabulary

Policies should be written against semantic roles, not implementation-specific tool names.

Preferred predicates include:

Avoid:

15.1 Residual-surface vocabulary

Policies may quantify over a trace’s residual surface — its declared negative space (Trace Specification §13). The residual surface is the collection:

bound by the first-order quantifiers already defined in §10.8 / §14.1 (∀ r ∈ residuals . …, ∃ r ∈ residuals . …). Within a quantified body, the following field accessors are available on the bound residual r:

AccessorMeaning
r.kindone of Assumption, Unverified, OutOfScope, Limitation, OpenQuestion
r.severityone of Info, Low, Medium, High, Critical
r.statusone of Open, Acknowledged, Addressed, Waived
r.targetthe target_ref the residual points at (may be empty)
r.related_artifact_idsthe affected/supporting artifacts (may be empty)
r.suggested_checkhow a reviewer could close the gap (may be empty)

severity is totally ordered: Info < Low < Medium < High < Critical. Comparisons such as r.severity ≥ High are interpreted against this order. status and kind are unordered enums compared by equality. ∅ denotes the empty value (a missing target/suggested_check, or an empty related_artifact_ids list).

A residual-surface policy expresses a requirement not on what the trace did, but on how honestly and navigably it declares what it did not do.

16. Binding to the Trace Specification

This section defines how the semantic DSL is grounded in the trace model.

16.1 Example mappings

Policy predicateTrace grounding
reasoning_action(a)action is a ReasoningAction
verification_action(a)reasoning action subtype is Verify
state_space_analysis_action(a)reasoning action subtype is StateSpaceAnalysis
formal_model_artifact(x)artifact constructor is FormalModelArtifact
approved_reference_artifact(x)artifact role is ApprovedReferenceRole or object is a reference artifact
ancestor_of(x, y)reachability through derived_from links
inputs(a)action_common.inputs
outputs(a)action_common.outputs
target(a)target carried in action-specific payload if present
policy_failed(p)policy evaluation status is Failed
residualstrace.residuals (the residual surface, Trace Spec §13)
r.severity, r.status, r.kindthe corresponding fields of a residual
r.severity ≥ Highseverity rank, where Info < Low < Medium < High < Critical

16.2 Binding rule

The policy DSL is interpreted over the canonical trace semantics, not directly over raw JSON.

JSON/Pydantic must first be decoded into the canonical trace model before policy evaluation.

17. Standard Example Policies

17.1 Pure temporal policies

Tests before commit

G(GitCommit -> P(RunTests /\ completed))

Every action has rationale

G(action -> rationale != empty)

Trace has lifecycle

start_event /\ F(end_event)

17.2 Scoped temporal policies

Research before edit

G(EditFile -> P_target(ReadFile \/ ReadDocumentation \/ SearchCode \/ AnalyzeCode))

Reasoning for high-stakes edits

G(EditFile /\ high_stakes_path(a) ->
  P_chain(VerificationResult \/ StateSpaceAnalysisResult \/ ConformanceResult))

17.3 Structural policies

Data flow integrity

G(forall input in inputs(a) ->
  exists! b in actions_before(a) . input in outputs(b))

Goals reference valid models

G(VerificationGoal ->
  target_artifact_id in {x.id | formal_model_artifact(x)})

Generated tests require state-space analysis

G(GeneratedTests ->
  exists x . ancestor_of(x, GeneratedTests) /\ state_space_analysis_result(x))

17.4 Residual-surface policies

These quantify over residuals (§15.1) to govern a trace’s declared negative space. They make the realistic bar — gaps declared, located, and triaged — enforceable, rather than requiring traces to be gap-free.

No open critical residuals

¬∃ r ∈ residuals . r.severity = Critical /\ r.status = Open

Intended as an approval gate: no critical declared gap may remain open at sign-off.

High-severity residuals acknowledged before commit

G(GitCommit -> ∀ r ∈ residuals . r.severity ≥ High -> r.status ≠ Open)

A commit must not silently carry an unacknowledged high- or critical-severity gap.

Unverified residuals have a suggested check

∀ r ∈ residuals . r.kind = Unverified -> r.suggested_check ≠ ∅

Every unverified claim must say how a reviewer could close it — turning the negative space into a work-list.

Assumptions are located

∀ r ∈ residuals . r.kind = Assumption -> (r.target ≠ ∅ \/ r.related_artifact_ids ≠ ∅)

Every relied-upon assumption must point at what it touches, so a reviewer can find it.

These four ship in the policy gallery. Beyond them, the residual-quantifier forms of §15.1 are evaluated generally by the reference compiler — any ∀ / ∃ / ∃! policy over residuals with field comparisons (=, ≠, ≥, …, and ≠ ∅) is enforceable, not only this standard set, and may be freely composed under temporal operators (e.g. G(GitCommit → ∀ r ∈ residuals . …)).

18. Interchange Model Notes

The canonical policy model is authoritative.

For interchange, policies may be projected into JSON/Pydantic as:

Use a structured canonical AST internally, and allow a textual representation externally.

That means:

18.2 Pydantic strategy

Recommended Python generation:

19. Recommended Implementation Strategy

19.1 Internal semantic layer

Use the canonical typed policy model in:

19.2 Parsing layer

Implement:

19.3 Binding layer

Implement policy evaluation against:

19.4 Serialization layer

Generate:

from the strict model, not the reverse.

20. Intended Outcomes

The intended outcomes of this policy specification are:

21. Summary

The clean conceptual distinction is:

Or, in one sentence:

Traces define the execution world; policies define the rules evaluated over that world.