PolySec

A security lens over the Polygraph toolset — it makes "this agent can't be talked into leaking your data" a property you prove, not hope. PolySec verifies and monitors the same SAM v2 strict-profile state machines Polygraph checks for correctness, and asks the questions the correctness tools do not. Not a fork — a lens over the same substrate, sharing its doctrines (controls before trust, observable rejection, no silent-clean paths, ground truth is executed code).

Its runtime arm, polyman (@cognitive-fab/polyman), enforces a proven policy live in a real agent — the only agent-security gate where the policy is model-checked unbreakable before it ships.

Where PolySec fits

PolySec and polyman are the security agents over the Polygraph gate: the same deterministic, SAM v2-founded engine that authors, checks, and runs state machines is what PolySec proves fully mediated and polyman enforces live.

Scope (read docs/polysec-spec.md §0). PolySec is a consistency check and a monitor, not a proof of security. It reasons over the control-flow layer (states, transitions, predicates over declared finite state) — it does not find implementation vulnerabilities. That residual is the trusted computing base, named and handed to a stronger method. "Exhaustive" means over the finite declared domains and the observable projection only.

Setup

Two independent things — you only need the first to run everything here:

1 — Run the checks. PolySec has no dependencies of its own; it loads the Polygraph engines from a sibling checkout at ../polygraph. Clone both side by side:

git clone https://github.com/jdubray/polysec.git
git clone https://github.com/jdubray/polygraph.git   # sibling — PolySec reuses its engines
cd polygraph && npm install && cd ..                 # Polygraph pulls in the SAM engine
cd polysec
npm test                  # 51 tests, green with NO ANTHROPIC_API_KEY

Node ≥ 20 (Node ≥ 24 to run polyman's TypeScript tests from source). If Polygraph lives elsewhere, point PolySec at it with POLYGRAPH_DIR=/path/to/polygraph npm test.

2 — Drive the machines with the Polygraph plugin (optional). For natural-language verification/rendering of these example machines inside Claude Code — not required for anything below:

/plugin marketplace add jdubray/polygraph
/plugin install polygraph@polygraph
/plugin install polyviz@polygraph     # optional — the deterministic diagram renderer
/reload-plugins

This adds the /verify, polynv, polygen, polyvers, and polyviz agents (see Drive the examples with the plugin).

Run the demos

npm run polysec:sandbox   # the lethal-trifecta demo (5-stage harden progression)
npm run polysec:fleet     # the agent-swarm demo (cross-instance over-egress)

Everything here only checks and explores — no model calls, no network, no clock. $0 API, and the test suite asserts it.

The conceptual spine

Security bugs in stateful systems are reachable-bad-state bugs: an auth bypass is an application-data-accepting state reached without an authenticating transition; a data leak is a state where a secret coexists with an egress capability. These are predicates over state — the objects Polygraph model-checks. The design target is not "the bad state is unreachable" (unprovable over a masked machine) but fully-mediated reachability: every modeled path to the forbidden region traverses a controllable, default-deny gate. The residual then decomposes into exactly two attackable things — gate bypasses (checkable) and unmodeled channels (made to fail closed) — plus the side-channel frontier below the state-machine layer.

Prevention lives in the acceptor; correction lives in the nap. The acceptor is the default-deny gate that stops a bad proposal before it lands. The nap is the forward-only corrective that fires once you're already in danger (via a masked edge). Recovery is containment, not restoration: from a state honestly carrying compromised = true, the best reachable safe state still wears the flag.

The five anchor use cases (spec §2)

Each is a complete, tested, self-checking example with positive and negative controls, all on SAM 2.1.2:

use case	invariant class	forbidden region	example
UC-1 lethal trifecta	coexistence	¬(untrusted ∧ sensitive ∧ egress)	polysec-sandbox
UC-2 secret custody	confidentiality / taint	¬(tainted ∧ egress_capable)	polysec-secret
UC-3 auth & ordering	reachability + ordering	no privileged action pre-auth; handshake ≺ app-data	polysec-auth
UC-4 capability broker	monotonicity + composition	no unapproved capability; no forbidden pair	polysec-broker
UC-5 agent fleet	cross-instance / aggregate	no collective over-egress	polysec-fleet

Each names the famous bug it catches: UC-1 prompt-injection exfiltration, UC-3 the SKIP-TLS state confusion, UC-4 the composition hazard invisible to per-capability reasoning, UC-5 the Hugging Face swarm.

The gates (all built)

Design-time — polysec harden (scripts/polysec-harden.mjs), the fully-mediated verdict over four checks:

1. from-init — reachable-bad-state hunt with the shortest counterexample.
2. havoc — maximal nondeterminism over the declared adversarial variables; a counterexample that uses a havoc edge names the unmediated variable. Catches unmodeled channels.
3. gate-deletion — delete the designated gates and test reachability; a surviving path is a bypass, with the witness naming the surviving transition.
4. recovery-convergence (scripts/polysec-recover.mjs) — from every danger state the corrective naps reach a desired state, nonblocking and nap-safe; records containment vs restoration as a first-class result.

Design-time — polysec diagnose (scripts/polysec-diagnose.mjs): the diagnosability gate (is region entry even detectable from the projection? returns the ambiguous state pair when not) + the diagnostic-adequacy grade (a wormhole-mutant family scored against a coupling sensor — kill ratio and survivors). Machine-agnostic.

Runtime — polysec guard (scripts/polysec-guard.mjs): a belief-set diagnoser + shield over a journal — alarms on a coupling sensor before the masked variable is directly observed, then fires a corrective nap.

Runtime — polysec fleet (scripts/polysec-fleet.mjs): the cross-instance aggregator — fleet invariants over a cohort's combined journals, with a fleet-level shield.

All deterministic, PR-gateable, nonzero exit on any failure. security.json is the one new declarative artifact (§4.2), a sidecar in the effects.manifest.json tradition.

The gates as commands

Every gate is a plain node script; the four scenario shortcuts wrap harden. All exit nonzero on any violation, so they drop straight into CI.

gate	command
harden a scenario	npm run polysec:{sandbox,auth,secret,broker}
harden any machine	node scripts/polysec-harden.mjs --module <next.cjs> --contract <c.json> --security <security.json> [--out <dir>] [--label <name>]
diagnose	node scripts/polysec-diagnose.mjs --module <next.cjs> --contract <c.json> --security <security.json> [--hide <projection-var>]
recover	node scripts/polysec-recover.mjs --module <next.cjs> --contract <c.json> --security <security.json>
guard (runtime)	node scripts/polysec-guard.mjs --module <next.cjs> --contract <c.json> --security <security.json> --journal <j.ndjson> [--sensors <s.mjs>]
fleet (runtime)	node scripts/polysec-fleet.mjs --journals <dir> --fleet <fleet.json> [--machine <instance.next.cjs>]

Each example ships the next.cjs, contract.json, security.json (and invariants.mjs) these commands consume — e.g. harden the broker directly: node scripts/polysec-harden.mjs --module examples/polysec-broker/next.cjs --contract examples/polysec-broker/contract.json --security examples/polysec-broker/security.json.

Drive the examples with the plugin

With the Polygraph plugin installed, these copy-paste prompts run its agents against PolySec's own machines. $0 API.

you want	prompt
render a machine + its invariants	Using polyviz, render the state machine and invariants for examples/polysec-broker (next.cjs, invariants.mjs).
verify a machine against traces	Verify examples/polysec-sandbox/next.cjs against examples/polysec-sandbox/contract.json and the traces in examples/polysec-sandbox/traces/.
elicit / grade invariants	Elicit invariants for examples/polysec-auth/next.cjs using examples/polysec-auth/contract.json.

/verify needs a trace corpus — only polysec-sandbox ships one (regenerate with npm run polysec:traces). For the other scenarios use polyviz (render) and polynv (invariants), which need only the machine + contract.

polyman — enforce the proof at runtime

@cognitive-fab/polyman is the runtime member of the family: it puts a proven PolySec policy between an agent and its tools as a default-deny, in-line tool gate.

import { createPolyman } from '@cognitive-fab/polyman';
import { wrapVercel } from '@cognitive-fab/polyman/vercel';

const pm = await createPolyman();                              // shipped, harden-proven policy
const res = await generateText({ model, tools, ...wrapVercel(pm, { session }) });
// a session that fetched untrusted content and read a secret CANNOT send email.

• Zero-config: ships the pre-proven lethal-trifecta policy + a starter tool-label map.
• Adapters: wrapVercel (in-process) and wrapMcp (the gateway / MITM shape — fronts any MCP server, e.g. a spec-driven capability server). Same mediate() kernel; a golden-parity test proves the runtime engine steps the machine byte-identically to the design-time checker.
• polyman verify: the coherence gate — will not serve a policy harden hasn't passed.
• runGuard: the belief-set diagnoser + shield, in the package.
• Self-contained, built to ESM+CJS+.d.ts, $0 API on the decision path.

Reuse, don't fork

PolySec adds the security gates and the security.json manifest; the heavy lifting is the Polygraph engines (../polygraph): the one BFS model checker (check.mjs), the one loader + stable() equality (load-spec.mjs), the {init,next} adapter (sam-adapter.cjs), and the graph enumerator (polynv/consequences.mjs). Havoc, gate-deletion, recovery, and the wormhole grade are all (module, steps) overrides handed straight to them — there is no second BFS and no second notion of state equality. Changes PolySec needs in Polygraph go in docs/ as a spec (Polygraph is readonly here), not as edits.

Repo layout

path	what
examples/polysec-*/	the five anchor use cases (machines, manifests, tests, self-checking demos)
scripts/polysec-*.mjs	the gates: harden, recover, diagnose, guard, fleet, lib
polyman/	the runtime enforcement package (@cognitive-fab/polyman)
test/	the assertions behind every claim (51 tests, $0 API)
docs/	the specs: polysec-spec, polysec-broker-spec, polyman-spec, polyman-plan

Doctrines (§4.7)

1. Prevention in the acceptor, correction in the nap.
2. Fully-mediated over unreachable.
3. Default-deny or it does not count.
4. State adequacy is the price of memorylessness.
5. Recovery is containment, not restoration.
6. Diagnosability before monitoring.
7. The residual is the TCB — name it, and hand its implementation to memory-safety, fuzzing, or audit.

Apache-2.0 · © Cognitive Fab LLC