Writing policies

A policy is the unit of Computable Governance — a formula (temporal logic over the finite trace, plus structural predicates) checked over a trace, which ponens evaluates to pass / fail with an exit code. Policies live in the public gallery or in your own local source — this page covers the formula language and how to write, add, and check your own.

The policy object

A policy is a JSON file named <id>.json:

{
  "id": "tests_before_commit",          // snake_case, must match the filename
  "name": "Tests Before Commit",
  "category": "workflow",               // see categories below
  "severity": "error",                  // error | warning | info
  "description": "Every commit must be preceded by a successful test run.",
  "formula": "G(GitCommit → P(RunTests ∧ completed))",
  "language_level": "pure_temporal",    // pure_temporal | scoped_temporal | structural
  "rationale": "Prevents untested code from entering the repository.",
  "tags": ["ci", "testing", "git"],
  "domain": "general",
  "examples": {
    "passes": "ReadFile → RunTests(pass) → EditFile → RunTests(pass) → GitCommit",
    "fails":  "ReadFile → EditFile → GitCommit (no test run before commit)"
  }
}

The formula language

Formulas are written over the trace's ordered actions, its artifacts, and its residual surface. Operators may be written with unicode or ASCII (→/->, ∧//\, ∨/\/, ¬/!, ≠/!=, ∅/EMPTY).

Atoms (what holds at an action)

Action types — ReadFile, EditFile, RunTests, GitCommit, Formalize, Verify, Decompose, GenerateTests, … (true when the current action is of that type)
Artifact types — VerificationResult, Decomposition, GeneratedTests, IMLModel, … (true when the action produces such an artifact)
Categories — reasoning, gateway, activity; and action (any)
Predicates — completed, failed, proved, refuted, sat, high_stakes_path
Lifecycle — start_event, end_event
Field non-empty — e.g. rationale ≠ ∅

Temporal operators

Operator	Meaning
`G φ`	globally — φ holds at every action
`F φ`	finally — φ holds at some action
`P φ`	previously — φ held at some earlier action
`H φ`	historically — φ held at every earlier action
`X φ`	next — φ holds at the immediately following action
`φ U ψ`	until — ψ holds eventually, and φ holds until then
`φ S ψ`	since — ψ held in the past, and φ has held since

Scoped operators (lineage-aware)

Operator	Meaning
`P_target φ`	some earlier action sharing the same target satisfied φ
`P_chain φ`	some earlier action in the dependency chain satisfied φ

Quantifying over the residual surface

Policies can govern a trace's declared negative space with ∀ / ∃ over residuals, with field access on the bound variable:

¬∃ r ∈ residuals . r.severity = Critical ∧ r.status = Open
∀ r ∈ residuals . r.kind = Unverified → r.suggested_check ≠ ∅

Fields: r.kind, r.severity, r.status, r.target, r.suggested_check, r.related_artifact_ids. Severity is ordered (info < low < medium < high < critical), so r.severity ≥ High works.

Worked examples

# pure temporal — tests before commit
G(GitCommit → P(RunTests ∧ completed))

# scoped — research before edit
G(EditFile → P_target(ReadFile ∨ AnalyzeCode ∨ SearchCode))

# reasoning required for high-stakes edits
G(EditFile ∧ high_stakes_path → P_chain(VerificationResult ∨ Decomposition))

# residual surface — no open critical gap at approval
¬∃ r ∈ residuals . r.severity = Critical ∧ r.status = Open

Write your own & use it

Create .ponens/policies/my_rule.json using the shape above.
Register a local source:
```
ponens sources add team --type local --path .ponens/policies
```
(or add a [[source]] block to .ponens/sources.toml).

Find it, add it to a trace, and check:

ponens policies search my_rule          # shows source = team
ponens policies add team/my_rule --into ./trace.json
ponens trace check ./trace.json

The materialized policy carries its provenance (source: team) into the trace, so a reviewer sees which source governed it.

Validate as you go

ponens trace check compiles each formula and reports syntax/semantic errors before evaluating. Unrecognized operators or unbalanced parentheses are caught there. Use ponens trace validate <file> to check the trace's own structure.

Reference

Categories: auditability, communication, conformance, reasoning, safety, security, structural, workflow. Severities: error, warning, info.

Language levels: pure_temporal (only temporal operators), scoped_temporal (uses P_target/P_chain), structural (quantifiers / first-order, incl. residual policies). The gallery records whether the reference compiler can evaluate each formula. See the Policy Specification for the full grammar.