Metadata-Version: 2.4
Name: ltl-harness
Version: 0.2.0
Summary: Temporal-logic guardrails for Claude Agent SDK agents — LTLf2DFA-compiled colored automata enforced via hooks.
Author: Peter Saghelyi
License-Expression: MIT
Project-URL: Homepage, https://github.com/askalot-io/ltl-harness
Project-URL: Repository, https://github.com/askalot-io/ltl-harness
Project-URL: Issues, https://github.com/askalot-io/ltl-harness/issues
Keywords: ltl,ltlf,guardrails,agents,claude,runtime-verification,declare
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Operating System :: POSIX
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Programming Language :: Python :: 3.14
Classifier: Topic :: Software Development :: Quality Assurance
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: claude-agent-sdk
Requires-Dist: ltlf2dfa>=2.0.0
Requires-Dist: pyyaml
Provides-Extra: dev
Requires-Dist: pytest; extra == "dev"
Provides-Extra: nl
Requires-Dist: nl2ltl>=0.0.6; extra == "nl"
Dynamic: license-file

# <img src="https://raw.githubusercontent.com/askalot-io/ltl-harness/main/docs/logo.png" alt="" width="40" align="top"> LTL Guardrail Harness

**Temporal-logic guardrails for [Claude Agent SDK](https://code.claude.com/docs/en/agent-sdk) agents.**
Rules like *"never issue a refund before the receipt has been verified"* live in a versioned
YAML rulebook — not in the system prompt. Each rule is compiled to a minimal deterministic
finite automaton by [LTLf2DFA](https://github.com/whitemech/LTLf2DFA)/[MONA](https://www.brics.dk/mona/),
advanced on every tool call via SDK hooks, and empowered to **deny** any call that would
permanently violate an enforced rule. No second LLM watching the first, no regex over
transcripts — a turnstile.

> **The agent proposes. The automaton disposes.**

This is the working implementation of the essay
[*Stop Begging Your Agent to Behave*](https://medium.com/@psaghelyi/stop-begging-your-agent-to-behave-b3664280c464)
(hooks, traces, and a little temporal logic: real guardrails for agentic workflows).

![run view — the seatbelt denying a refund under prompt pressure](https://raw.githubusercontent.com/askalot-io/ltl-harness/main/docs/dashboard-run.png)

## How it works

```
rules/*.yaml          policy: activities (world→symbol map) + DECLARE/LTLf rules
      │
      ▼  LTLf2DFA + MONA (design time, cached)
colored automata      minimal DFAs, states labeled with the four RV-LTL verdicts
      │
      ▼  Claude Agent SDK hooks (runtime, deterministic, no model in the loop)
PreToolUse            simulate the proposed call; deny if every possible outcome
                      permanently violates a seatbelt rule — and name the rule
PostToolUse           resolve the actual activity, advance every machine, append
                      the verdicts to the flight recorder (JSONL per run)
Stop                  block the run from ending while an "eventually" is unmet —
                      under finite-trace semantics the end of the run is judgment day
```

After every event each rule wears one of four colors:

| color | meaning |
|---|---|
| `PERM_SAT`  | fulfilled, whatever happens next |
| `CURR_SAT`  | fine so far, could still go wrong |
| `CURR_VIOL` | an obligation is open — fine mid-run, **a violation if the trace ends now** |
| `PERM_VIOL` | broken beyond repair (trap state) |

Each rule carries a **posture**, promoted like a release pipeline as confidence grows:
`recorder` (log only) → `tripwire` (alert on red) → `seatbelt` (deny / block).

## Install

```bash
pip install ltl-harness        # Python ≥ 3.11; also needs MONA: `apt install mona`
```

That gives you the engine, the SDK hooks and four commands: `ltl-harness-lint`,
`ltl-harness-server`, `ltl-harness-demo` and `ltl-harness-nl2rules`. Installed this way,
flight records go to `./runs`, a `.env` is read from the current directory if there is
one, and the rulebook defaults to the bundled refund example — point
`LTL_HARNESS_RULEBOOK` (and `LTL_HARNESS_RUNS`) at your own. The `nl` extra installs
with uv only: `nl2ltl` declares `Python <3.11`, which pip enforces and uv does not.

## Quick start (from a checkout)

Prerequisites: [uv](https://docs.astral.sh/uv/) (it fetches Python 3.14; any Python ≥ 3.11 works), and MONA
(`apt install mona` — Debian/Ubuntu; the compiler behind LTLf2DFA).

```bash
cp .env.example .env                       # add your Claude Code OAuth token
cd py
uv sync --extra dev                        # installs Python 3.14 (.python-version) + locked deps into .venv

.venv/bin/python -m pytest tests/                              # engine tests
.venv/bin/python -m ltl_harness.lint_cli ../rules/refund.rules.yaml   # verify the rulebook
.venv/bin/python -m ltl_harness.agent happy                    # run a live demo scenario
.venv/bin/python -m ltl_harness.server                         # dashboard on :8471
```

### Demo scenarios

The demo is the essay's refund agent: mock MCP tools, real Claude, and a rulebook it
cannot escape. Note what the system prompts are *not*: there is no IMPORTANT, no NEVER,
no MUST — the rules hold anyway.

| scenario | what happens | mechanism demonstrated |
|---|---|---|
| `happy`  | receipt verifies on the 2nd attempt; lookup → verify → refund → audit note | recorder: colored trace, all green |
| `rogue`  | verification keeps failing AND the prompt tempts the agent to refund anyway | **seatbelt**: `PreToolUse` denies `issue_refund`; the agent escalates instead |
| `sloppy` | prompt says to skip audit/bookkeeping steps | **Stop hook**: the run may not end while an obligation is open |

## The rulebook

Activities are the security boundary — the world→symbols mapping is deliberately dumb
(tool-name equality plus, optionally, one field of the tool result):

```yaml
activities:
  verify_receipt_ok:
    tool: mcp__refund__verify_receipt
    result: { path: verified, equals: true }
```

Rules are DECLARE templates (`Existence`, `Absence(n)`, `Response`, `Precedence`,
`ChainResponse`, `NotSuccession`, `Init` — list-valued params mean *any of*)…

```yaml
- id: no-refund-before-verification
  description: Never issue a refund before the receipt has been verified.
  template: Precedence
  params: { a: verify_receipt_ok, b: issue_refund }
  posture: seatbelt
```

…or, since every rule goes through a real LTLf compiler, any raw formula:

```yaml
- id: order-lookup-happens
  description: Every run must look up an order at least once.
  formula: "F(look_up_order)"
  posture: recorder
```

### Lint the rulebook before the flight

All machines run side by side as one product automaton, so whole-rulebook questions are
mechanical. `lint_cli` checks for **contradictions** (no compliant run exists at all),
**traps** (a reachable healthy state from which every continuation violates something —
reported with a counterexample trace), **dead rules**, and **shadowed rules**. The demo
agent refuses to start on a rulebook that fails verification; run it in CI on every edit.

## Natural language → rules (NL2LTL, design time)

The essay's role reversal: the LLM translates policy *at design time*, where a human
reviews the output once; deterministic code does the checking at runtime.

```bash
cd py && uv sync --all-extras              # adds nl2ltl (the `nl` extra) to the same .venv
.venv/bin/python -m ltl_harness.nl2rules \
  "Every refund must eventually be audited." --id audit-eventually --posture recorder
```

A Claude-backed [`nl2ltl`](https://github.com/IBM/nl2ltl) engine picks the DECLARE
pattern over the rulebook's vocabulary; the formula is paraphrased **back** to English
*without seeing your sentence* (the round-trip check — if the two sentences don't say
the same thing, the original wins and a human looks closer); on approval the rule is
appended and the runtime linter re-verifies the whole rulebook, reverting the append
if verification fails. Guardrails on the guardrails.

`nl2ltl` is an optional extra: the runtime never imports it. The two sides only talk
via files and subprocesses, mirroring the design-time/runtime split. (They used to need
separate venvs; `ltlf2dfa` 2.0 moved to modern `lark` and removed the conflict —
[whitemech/LTLf2DFA#78](https://github.com/whitemech/LTLf2DFA/issues/78).)

## The dashboard

![rulebook view — every rule is a little machine](https://raw.githubusercontent.com/askalot-io/ltl-harness/main/docs/dashboard-rulebook.png)

- **Rule status over the trace** — rules × events matrix in the four colors; ⛔ columns
  mark calls the seatbelt denied (events that never happened). Click to time-travel.
- **State machines** — every rule's compiled DFA rendered live, current state
  highlighted, taken transition in blue.
- **Flight recorder** — every event, denial (with the rule that fired and why),
  stop-block, and the agent's final reply. One JSONL file per run: a complete account
  of what the agent actually *did*, independent of what it *said* it did.
- **Rulebook tab** — formulas, diagrams, and the live design-time verification verdict.

No build step, no frontend dependencies; the server is stdlib-only.

## Using it in your own agent

```python
from ltl_harness.engine.rulebook import load_rulebook
from ltl_harness.engine.lint import lint_rulebook
from ltl_harness.hooks import create_guardrails
from ltl_harness.recorder import Recorder
from claude_agent_sdk import ClaudeAgentOptions, query

rulebook = load_rulebook("rules/my.rules.yaml")
assert lint_rulebook(rulebook)["ok"], "rulebook is broken — refusing to fly"

recorder = Recorder("runs", "my-run", meta={...})
hooks, monitor, finalize = create_guardrails(rulebook, recorder)

async for message in query(prompt=..., options=ClaudeAgentOptions(..., hooks=hooks)):
    ...
verdicts, ok = finalize()   # judgment day: open obligations become violations
```

## Deployment

`deploy/` has the reference configs used in production:

- `ltl-harness.service` — systemd unit running the dashboard on `127.0.0.1:8471`
- `nginx-ltl-harness.conf` — nginx reverse proxy exposing it (port 8080)

```bash
cp deploy/ltl-harness.service /etc/systemd/system/   # adjust paths
systemctl enable --now ltl-harness
cp deploy/nginx-ltl-harness.conf /etc/nginx/sites-available/ltl-harness
ln -s /etc/nginx/sites-available/ltl-harness /etc/nginx/sites-enabled/
nginx -t && systemctl reload nginx
```

## Repository layout

```
rules/            the rulebook (YAML) — policy as code, owned by humans
py/ltl_harness/   the harness
  engine/           formulas.py (DECLARE→LTLf) · dfa.py (MONA→colored DFA)
                    rulebook.py · monitor.py · lint.py
  hooks.py          PreToolUse / PostToolUse / Stop for the Agent SDK
  recorder.py       JSONL flight recorder
  agent.py          demo refund agent (mock MCP tools, three scenarios)
  server.py         dashboard server (stdlib)
  lint_cli.py       CI entry point — exit 1 on contradiction/trap
  nl2rules.py       NL → DECLARE → LTLf translator (needs the `nl` extra)
  paths.py          where rules/, runs/ and .env are found (checkout vs installed)
  ui/               the dashboard (plain HTML/JS, no build)
py/tests/         engine test suite
runs/             flight records (gitignored)
deploy/           systemd + nginx reference configs
docs/             screenshots
```

## Honest limits

- **The activity mapping is the weak joint.** The automaton sees symbols; reality sends
  tool calls. Keep the mapping embarrassingly simple and audit it like the security
  boundary it is.
- **It governs the trace, not the text.** No temporal rule notices a rude email or a
  hallucinated clause. Content quality needs its own tools.
- **Rules only cover what someone thought to write.** The rulebook is a floor, not a
  ceiling — the flight recorder is where the missing rules announce themselves.

## References

- De Giacomo & Vardi, [*Linear Temporal Logic and Linear Dynamic Logic on Finite Traces*](https://www.ijcai.org/Proceedings/13/Papers/132.pdf) (IJCAI 2013) — LTLf semantics
- Pesic, Schonenberg & van der Aalst, [*DECLARE: Full Support for Loosely-Structured Processes*](https://doi.org/10.1109/EDOC.2007.14) (EDOC 2007) — the template catalog
- Maggi, Montali, Westergaard & van der Aalst, [*Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata*](https://doi.org/10.1007/978-3-642-23059-2_13) (BPM 2011) — the four-color runtime monitoring
- Fuggitti & Chakraborti, [*NL2LTL — a Python Package for Converting Natural Language Instructions to LTL Formulas*](https://ojs.aaai.org/index.php/AAAI/article/view/27068) (AAAI 2023) — [github.com/IBM/nl2ltl](https://github.com/IBM/nl2ltl)
- [LTLf2DFA](https://github.com/whitemech/LTLf2DFA) / [MONA](https://www.brics.dk/mona/) — the formula→DFA toolchain
