← Guides

Govern a repo with policies

You'll end up with a set of best-practice rules — research before editing, tests before commit, no open critical gaps — checked over every trace as a real PASS/FAIL, offline. This is Computable Governance.

1. Pull the gallery

ponens registry update                         # fetch the public gallery
ponens policies search testing                 # browse by keyword
ponens policies search --severity error

Browse the full set in the policy gallery. Each policy is a formula in LTLf with a plain-English rationale and pass/fail examples.

2. Add policies to a trace

ponens policies add tests_before_commit --into trace.json
ponens policies add research_before_edit --into trace.json
ponens policies add no_open_critical_residuals --into trace.json

3. Check — the gate

ponens trace check trace.json                  # → PASS / FAIL (non-zero exit on FAIL)

Each policy compiles to an automaton and is evaluated over the trace. A result is pass, fail (with the witnessing position), or not_applicable when the trigger never occurs. Wire this into CI to make it a required check.

4. Write your own

A policy is a small JSON file with a formula. For example, "every commit is preceded by a passing test run":

{
  "id": "tests_before_commit",
  "name": "Tests Before Commit",
  "category": "workflow",
  "severity": "error",
  "formula": "G(GitCommit → P(RunTests ∧ completed))",
  "language_level": "pure_temporal",
  "rationale": "Prevents untested code from entering the repository.",
  "examples": { "passes": "… RunTests(pass) → GitCommit", "fails": "EditFile → GitCommit" }
}

Register a local source and use it just like a gallery policy:

ponens sources add team --type local --path .ponens/policies
ponens policies add team/tests_before_commit --into trace.json

The full operator set, the structural/residual predicates, and the grammar are in the Policy Language reference; the step-by-step authoring walkthrough is in Writing policies.

Policies can require reasoners

A policy can demand formal evidence, not just process — e.g. a high-stakes edit must be backed by a proof or a model check in its lineage. Those proofs come from reasoners (CodeLogician, ImandraX, Z3, TLC), which a policy can require. That's the bridge from "did the steps" to "proved the property."

Next: enforce it on every PR →