ceco proof gate

Runtime policy enforcement extracted from ceco-offline (development @ 484bb16, 2026-07-04).

This package is the proof gate only: an MCP server that evaluates agent actions against a Policy State Machine, emits a tamper-evident audit trail, and optionally dispatches approved transitions to internal / federated handlers.

It does not include the ceco compile / synthesis pipeline (ceco derive, SMT/Lean generation, ceco-mcp analysis server, or supplier-onboarding demo).

What is included

Area	Modules
Gate MCP + SSE daemon	`gate_mcp_server`, `gate_daemon`, `gate_config`
Transition evaluation	`runtime`, `dsl`, `sexp`, `simulate` (concrete), `validator`
Federation / handlers	`mcp_client`, `mcp_federation`, `internal_mcp_server`, `internal_handlers`
Context & anchors	`context_resolvers`, `policy_anchor`, `code_guards`, `proof_cache`
Audit / attestation	`audit/` (hash chain, CPAR/CCPB, optional ZK backends)

Docs

Proof Gate API — MCP tool reference
MCP Architecture — tiered gate / internal / domain
Gate Runtime Performance — SSE daemon, machine cache, transition index
Gate Security Findings
Audit Trail
Proof Gate State Machine
Full specification — Part II is the runtime gate; Parts I/III describe the offline compile pipeline (not shipped here)
Operating notes

Install

cd /home/martyn/repos/ceco
poetry install
# or: pip install -e ".[dev]"

Quick start (payment example)

export CECO_GATE_CONFIG=examples/gate_config.payment.yaml
export CECO_GATE_INTERNAL_MODE=inprocess

# stdio MCP (Cursor / Claude Desktop spawn this)
poetry run ceco-gate-mcp

# or persistent SSE daemon for multi-turn agents
poetry run ceco-gate-daemon
curl http://127.0.0.1:14780/health

Point an MCP client at stdio ceco-gate-mcp, or at http://127.0.0.1:14780/sse for the daemon.

Entry points

Script	Module
`ceco-gate-mcp`	`ceco.gate_mcp_server:main`
`ceco-gate-daemon`	`ceco.gate_daemon:main`
`ceco-internal-mcp`	`ceco.internal_mcp_server:main`

Tests

poetry run pytest tests/ -q

Provenance

Source: /home/martyn/repos/ceco-offline branch development commit 484bb16. Feature branches feat/gate-daemon, feat/machine-cache, and feat/transition-index are already merged into that tip. Local uncommitted edits in ceco-offline that removed the machine cache / transition index were not carried over.