singularityhacker

Lean Guard — AI skill for Claude Code

AI community

A policy layer for AI coding agents, written and proved in Lean 4. Every Claude Code tool call is checked by a decision function with machine-checked guarantees: no exfiltration after reading a secret.

How to install Lean Guard

This entry records only its repository, not the path inside it, so there is no exact command to give. Open singularityhacker/lean-guard and copy the folder into ~/.claude/skills/, or the file into ~/.claude/agents/.

What Lean Guard does

Alternatives in AI

Cursor Talk To Figma MCP — TalkToFigma: MCP integration between AI Agent (Cursor, Claude Code, Codex) and Figma, allowing Agentic AI to c 7k ★
ARIS Agent Guide — For AI agents reading this repo 6.2k ★
System — You are YouClaw, a helpful AI assistant 684 ★

README

lean-guard

[![ci](https://github.com/singularityhacker/lean-guard/actions/workflows/ci.yml/badge.svg)](https://github.com/singularityhacker/lean-guard/actions/workflows/ci.yml)

A policy layer for coding agents, written and **proved** in Lean 4.

Every tool call Claude Code makes goes through a Claude Code `PreToolUse` hook to a native Lean binary. The binary decides **allow** (defer to Claude Code's normal permissions), **ask** (hand the call to a human) or **deny**, and keeps per-session state. The decision function comes with machine-checked proofs. It complements a VM or container: the VM limits what *can* happen, and the guard decides what *should*.

Claude Code ──PreToolUse JSON──► lean-guard ──► parse → Action        (trusted, Guard/Hook.lean)
                                              decide / step          (proved,  Guard/Core.lean)
                                              ◄── "" | ask | deny

What is proved

All theorems are in [`Guard/Theorems.lean`](Guard/Theorems.lean). They hold for **every** policy, state and action, not just test cases. `tests/Axioms.lean` checks that none of them uses `sorry`.

Theorem	Guarantee
`deny_wins`	If a deny rule matches, the answer is `deny`, never `ask` or `allow`.
`unlisted_tool_not_allowed`, `unlisted_program_not_allowed`, `malformed_not_allowed`	Default deny: anything not on an allow-list, or anything the parser can't understand, never runs without a human.
`write_contained`, `exec_contained`, `read_contained`	Allowed writes, and allowed commands with every path they mention, are inside the workspace by component prefix (`/ws-evil` is not inside `/ws`).
`resolve_clean`	Path normalization leaves no `.`, `..` or empty components.
`no_exfiltration`	In any session, once an action that may read a secret goes ahead, every later action that may send data off the machine is denied, whatever happened before or in between.
`budget_respected`	Across any t