🐍 🏠 🍎 🪟 🐧 - Deterministic AI safety policy engine with Z3 formal verification: write, verify and enforce…
CSL-Core
以下摘录自该仓库的 README(片段) · 在 GitHub 读完整 README →
**Find, prove and control the AI agents on your machines.**
CSL-Core finds every AI agent on a host and what it can reach, writes a policy for each one,
proves the policies with Z3 and TLA+, tests the code that connects agents to policies against
bypass tricks, and enforces them deterministically, outside the model. The model never sees the
rules, so it cannot talk its way past them.
Quick start
cslcore setup is the whole first install: it scans the machine, explains what it found, and opens
the protection board, the riskiest agents first. Enter gives every agent standard limits, a policy
made from them and checked with Z3, and the change that puts the guard in its call path, shown as a
diff with a one-line summary before anything is written. A number opens one agent instead: its
limits in your own numbers (amounts, any numeric argument, allow, approval or block per tool), the
policy, the wiring and a check that decides sample calls with the real policy and shows what runs
and what stops. Until you confirm a wiring change it writes only inside the folder you run it in.
It is resumable at any step, and cslcore setup later opens the board where you left it.
Then watch it run:
Want to look first, without installing anything? With uv:
The scan on its own: read-only, about a second. Add --share to get a card of your machine's reach
map to post (no host name, user names or paths on it; --anonymize also hides agent names). To try
the whole flow on a sample host instead of your machine, from a clone of this repository (the sample
host and the traffic script are in the repository, not in the package):
Already on 0.5.1? Upgrading changes nothing: setup recognises your integration, keeps your policies
where they are and tests your own mapper. See MIGRATION.md.
Why
Rules in a prompt are suggestions. Models can be talked out of them, they hold most of the time
rather than every time, and nothing records what happened. CSL-Core keeps the rules outside the
model, in compiled policies that are proven consistent before they run and checked on every tool
call, the same way every time.
Three things usually go wrong before a single rule is written, and CSL-Core covers them too:
1. **Nobody knows which agents are running.** Assistants, MCP servers, scheduled jobs and scripts
with tool access accumulate on every machine.
2. **The policy is proven, the glue code is not.** The code that turns a real call like
Write(file_path="/srv/app/../etc/passwd") into policy variables is where guards are bypassed.
3. **Strict rules break real work.** Switching enforcement on without seeing what it would block
gets it switched off again.
How it works
1. Discover: cslcore venom
Reads code (parsed, never run), assistant and MCP configs, cron, systemd and launchd, the process
list, run history and existing policies. Every agent gets its tools classified by risk (read,
write, external, execute, spend, destructive), its guard coverage, and findings from "agent runs as
root" to "an inbound webhook reaches a public posting tool". Nothing on the host is changed;
credential values, prompts and transcripts never reach any output. Reports land in
.csl/venom/reports/, and cslcore venom --check gates CI. A scan is a snapshot, so each later
scan also names what opened since the last one (a plugin installed, a credential added);
--check --fail-on-new-reach fails CI on it. Between scans the guard covers the gap: a tool it
was not mapped for is denied, not allowed.
When discovery finishes, the web draws back into one point and spreads again along what can really
reach what: the **reach map**, with the strongest chain lit as a purple artery.
See what can reach what: cslcore venom map
Each agent on its own may look harmless. The risk is in the chain: an agent that reads web content
can change the code of another agent that runs as root, or holds a cloud credential, or moves money.
Venom builds the **reach graph** from what discovery found (who receives untrusted input, whose
declared file scope or account covers whose files, who runs as root, which tools have no rule) and