LeanGuard: a Lean-verified policy that gates a coding agent's tool calls

LeanGuard is a Claude Code plugin that checks every tool call before it runs. It uses a Lean-verified engine for a guarantee testing cannot provide: no policy, not even one that allows everything, can let the agent disable its own guard. A proof can establish that for every policy; a test suite can only sample. The problem it addresses is destructive actions a coding agent can take: deleting a failing test, rm -rf on a directory, disabling CI, force-pushing over history, or reading a secret and sending it out. The gate covers every tool call, including Bash, Write, Edit, Read, WebFetch, MCP tools, and tools it has never seen.

The check runs in a PreToolUse hook, which Claude Code evaluates before a tool executes and independently of the model. The agent cannot edit the policy or route around the hook.

The verified core

The decision is a Lean 4 function. Given a policy and a reified tool call, it returns allow, ask, or deny. The policy is data: an ordered list of rules decoded from JSON at runtime, the same engine-versus-policy split AWS Cedar uses. The kernel checks the function on build, and its properties hold for every policy, so the policy file can be retuned for any project or language without changing a proof. There are nine theorems in total; four are the top-level guarantees:

• self_protection_deny: a write or delete to LeanGuard’s own policy, checker, or hook files is denied, for every policy, including one that allows everything. The self-protect rule is prepended in engine code that the policy language cannot name, so no policy edit can remove it.
• forbid_trumps_permit: any firing deny rule forces a deny, regardless of order or how many allow rules match.
• allow_characterization: an allow implies no deny and no ask rule fired, which pins the deny > ask > allow precedence.
• default_deny: a malformed or empty policy denies everything.

The theorems use only Lean’s three standard axioms, with no sorry.

Covering tools it has never seen

The policy has no per-tool table. Any call is modeled generically: infer an operation from the tool name (the most-destructive verb across the name tokens, or unknown when unsure), then extract the resources it touches by walking the arguments recursively and canonicalizing paths (.., ~, symlinks, case). A call fans out into one verified request per resource, and the most restrictive verdict wins. Two rules keep a heuristic error from becoming an allow. A non-native tool is unverified and its write, delete, or network call never auto-allows. Anything the translator cannot resolve to a concrete resource, an opaque argument or a destructive op with no locatable target, also gates. The only path to allow is a native tool with a positive rule match. An unseen MCP tool deleting outside the workspace, or attaching ~/.ssh/id_rsa to an email, is handled the same way as a Write outside the workspace.

What it does not do

LeanGuard is a decision point. It returns a verdict and does not contain a process that ignores it. An allowed interpreter (python x.py, make, npm run build) runs code whose effect is not in the tool arguments, so self_protection_deny does not apply to it. The proofs cover the request the engine evaluates. They do not cover the Python that builds that request from a tool call, or the OS that runs the allowed command. Those layers are unverified. Containment of an allowed command is delegated to Anthropic’s @anthropic-ai/sandbox-runtime, which LeanGuard configures from the same policy: it wraps the whole process in Seatbelt or bubblewrap and denies writes and network by default. Guard-file immutability requires separate file ownership. A chmod the agent’s own uid can undo does not provide it.

Where it fits

Pre-action authorization for agent tool calls is a large, mostly unverified category. LeanGuard applies Cedar’s verified-engine and policy-as-data pattern to a coding agent’s filesystem and tool effects. The one property with no prior machine-checked instance found is self_protection_deny, a policy-independent self-protection theorem for a system whose adversary can edit its own policy data. The theorem is small and fires only on a write-shaped call, and the OS layer is what protects the guard files. A second reason to prefer a proof is scale: proof coverage holds as the policy language grows, where test coverage of a more complex decision function would degrade, which is why larger authorization systems run on verified cores. That benefit is latent while the rule set is small. LeanGuard has a small verified core and delegates enforcement to the OS. It is not a formally verified sandbox.

The engine, the gate, 46 tests, and the nine theorems are in the repo.