Content
# podman-ai-agent-isolation
Run AI coding agents (Claude Code, OpenAI Codex) inside a rootless Podman container that has read-write access to a single project checkout and nothing else on the host. The host's SSH agent is forwarded for git auth so you don't have to copy keys into the container.
Because the container *is* the boundary, the agents inside run with their interactive permission prompts disabled — Claude with `--dangerously-skip-permissions`, Codex with `--yolo`. Hand off a task and walk away; you do not babysit every file edit and shell command with a "yes / no" prompt. The blast radius is the project tree (which `git` can revert) and the persistent `ai_agent_*` volumes — nothing else on the host is reachable.
Git is the actual safety net — commit before each session, `git diff` after, `git reset --hard` if needed.
> **Scope.** The image as shipped is built for the author's workflow: Lean 4, LaTeX, tree-sitter, Ott, and the surrounding CLI / MCP tooling. The reusable parts are the structure — entrypoint with UID/GID mapping, wrapper script, volume layout, permission-bypass posture, `.ai-agent.json` skill plumbing — none of which assume Lean. Strip the toolchain bits you don't need from `Containerfile.ai-agent` and add your own; the rest of the setup carries over unchanged.
## Isolation boundary
The project checkout is **bind-mounted** at `/work`, not copied. That means:
- Edits the agent makes inside the container are visible *immediately* on the host — your editor, IDE, file watchers, and `git` on the host all see them in real time.
- Edits you make on the host (in your editor / IDE) are visible *immediately* to the agent inside the container.
- `git` works equally well on either side — you can stage/commit/push from your shell on the host, from inside the container, or mix the two. The repo is the same `.git` directory either way.
- For Lean projects, the per-project Lake build state in `<project>/.lake/build/` is shared via the same bind mount. Compile on the host and the container picks up the existing `.olean` files; or vice versa. Mathlib's `lake exe cache get` unpacks oleans directly into `<project>/.lake/build/`, so the cache fetch only ever happens once across the boundary regardless of which side ran it. The host's `~/.elan` is bind-mounted read-only so the toolchain version always matches — the prerequisite for olean reuse.
Everything *outside* the mounted checkout is isolated:
- Other directories under `$HOME` — invisible.
- Other projects — invisible.
- System files — invisible.
- The host's `~/.claude/` and `~/.codex/` — invisible. The container has its own auth and settings dirs (`/home/user/.config/<project>-claude` and `<project>-codex`, persisted in the `ai_agent_config` Podman volume).
A useful corollary: your **non-isolated** `claude` / `codex` install on the host keeps working exactly as before. They read `~/.claude` / `~/.codex` on the host, which the container never touches. You can run a host-side Claude session in one terminal and a jailed Claude session against the same repo in another, with completely independent auth, settings, sessions, and history.
(The host's `~/.elan` is bind-mounted *read-only* by default so existing Lean toolchains are reused without exposing the rest of `$HOME`. Set `AI_AGENT_HOST_ELAN=off` to use a dedicated volume instead.)
The host's SSH agent socket is forwarded into the container so git over SSH works without copying private keys. Your network, however, is not isolated — `--network host` is enabled so agents can reach localhost services. Tighten that in the wrapper if you want stricter network isolation.
## Where persistent state lives on the host
The `/home/user/...` paths inside the container are **not** mapped to your host `~/...`. They are backed by Podman named volumes that live under rootless Podman storage, by default at `~/.local/share/containers/storage/volumes/<volume>/_data/`. The wrapper mounts each volume with `:rw,U` under `--userns=keep-id`, so files inside are owned by your host user — you can read and edit them directly, no `podman unshare` needed.
| Container path | Backed by | Contents |
|--------------------------|---------------------------|----------------------------------------------------------------------------------------------|
| `/work` | bind mount of project dir | Your checkout — lives at the host path you started from, not in any volume |
| `/home/user/.config` | `ai_agent_config` | Claude / Codex auth, settings, MCP config, per-project memory files, status line, gh state |
| `/home/user/.ssh` | `ai_agent_ssh` | `known_hosts` (private keys stay on the host via SSH agent forwarding) |
| `/home/user/.agents` | `ai_agent_skills` | Codex skills directory |
| `/home/user/.cache/elan` | `ai_agent_cache_elan` | Elan downloads cache |
| `/home/user/.cache/lake` | `ai_agent_cache_lake` | Lake / Mathlib binary cache |
| `/home/user/.cache/uv` | `ai_agent_cache_uv` | `uv` cache (MCP servers like `lean-lsp-mcp`) |
| `/home/user/.elan` | host `~/.elan` (ro) or `ai_agent_elan_home` (when `AI_AGENT_HOST_ELAN=off`) | Elan toolchains |
Inspect any of them from the host:
```bash
# Resolve a volume to its on-disk path
podman volume inspect ai_agent_config --format '{{.Mountpoint}}'
# Or peek inside a running container
podman exec <container-name> ls /home/user/.config/
```
For example, Claude Code's per-project memory for a project named `poison` ends up at:
```
~/.local/share/containers/storage/volumes/ai_agent_config/_data/poison-claude/projects/-work/memory/
```
These volumes survive container exit (`--rm`), `--replace`, image rebuilds, and host reboots. They go away only if you explicitly `podman volume rm <volume>` or `podman volume prune` while no container references them.
## What's in the image
- **Claude Code** (native installer, runs with `--dangerously-skip-permissions` inside the jail) and **OpenAI Codex** CLI
- **uv / uvx** with `lean-lsp-mcp` MCP server pre-wired for both agents
- A **pre-installed Elan / Lean 4** toolchain seeded on first run (host `~/.elan` is bind-mounted read-only by default; set `AI_AGENT_HOST_ELAN=off` for a dedicated volume)
- Common AI-agent CLIs: `git`, `gh` (+ `gh-sub-issue`), `rg`, `jq`, `fd`, `ast-grep`, `difftastic`, `scc`, `yq`, `hyperfine`, `watchexec`, `comby`, `rga`, `tree-sitter-cli`, …
- LaTeX (`latexmk`) for paper / proof workflows
- An entrypoint that maps the host UID/GID into the container so `/work` files aren't root-owned
## Prerequisites
- **Linux host.** Developed and tested on Linux. No claims are made about macOS or Windows.
- Podman (rootless is fine).
- `jq` on the host (the build script and wrapper read `.ai-agent.json` with it).
## Quick start
```bash
# 1. (optional) Drop a .ai-agent.json into your project to set the project name
# and any extra Claude Code skills to bake into the image; see below.
# 2. Build the image and create persistent volumes (the build script does both)
./scripts/build-ai-agent-container ~/src/myproject
# 3. Install the wrapper somewhere on PATH
ln -sf "$(pwd)/scripts/ai-agent-jailed" ~/bin/ai-agent-jailed
ln -sf ~/bin/ai-agent-jailed ~/bin/claude-jailed
ln -sf ~/bin/ai-agent-jailed ~/bin/codex-jailed
# 4. Run an agent inside any project checkout
cd ~/src/myproject
claude-jailed # or: codex-jailed, or: ai-agent-jailed bash
```
First run prints `[entrypoint] Seeding /home/user/.elan from /opt/elan-seed …` once and takes a few seconds. After that, startup is instant.
The first time you launch each agent you'll need to authenticate the usual way (Claude opens a browser auth flow; Codex prompts for OpenAI sign-in). The credentials are written into `/home/user/.config/<project>-claude` / `<project>-codex` inside the `ai_agent_config` volume and persist across container restarts and image rebuilds — you only re-authenticate if you change `.ai-agent.json`'s `project`, wipe the volume, or the upstream token expires.
## Configuration (`.ai-agent.json`)
`.ai-agent.json` lives at the **target project root** (the dir mounted at `/work`), not in this infra repo. It is optional — if missing, both scripts default to `project = basename(PROJECT_DIR)` and an empty `extra_skills` list.
```json
{
"project": "myproject",
"extra_skills": [
"~/.claude/skills/proof-step",
"~/.claude/skills/proof-step-review",
"~/.claude/skills/proof-planning"
]
}
```
- `project` (optional) — short project name. Image is tagged `localhost/<project>-agent:latest`; container name is `<project>-agent-<agent>-<workspace-tag>`; in-container Claude / Codex config dirs are namespaced `<project>-claude` / `<project>-codex` so multiple host projects can share `ai_agent_config` cleanly. Defaults to `basename(PROJECT_DIR)` when absent.
- `extra_skills` (optional) — list of full host paths to Claude Code skill directories to bake into the image. Leading `~` is expanded. Each is staged with `cp -rL` (symlinks dereferenced); the basename becomes the skill name inside the container. Missing paths are skipped with a notice. The entrypoint links every baked skill into both Claude Code and Codex skill dirs at startup, so adding a path and rebuilding is the only step needed to make a new skill available. Omit the field (or set it to `[]`) if you don't want any.
The build script picks up `.ai-agent.json` from its argument (`./scripts/build-ai-agent-container ~/src/myproject`); the wrapper picks it up from whichever directory ends up mounted at `/work`. One image per `project` value is built, then any number of host projects that share that name reuse it.
## Using the wrapper
```bash
ai-agent-jailed claude # default: --continue prepended
ai-agent-jailed codex ~/src/another-project # mount a different checkout at /work
ai-agent-jailed bash # shell inside the container
# Pass args to the agent (wrapper injects --continue or "resume --last" before them)
claude-jailed --help
codex-jailed --version
# Pass-through after `--` — wrapper adds nothing after its fixed prefix
claude-jailed -- -r 52ea7f53-2b6a-4732-9eb7-f7292bd85d36
codex-jailed -- resume 019d0c58-596c-7d11-9d9f-75370b031212
# Replace an existing container with the same name
claude-jailed --replace
```
Per-invocation env vars: `AI_AGENT_PROJECT_DIR` (override mounted dir), `AI_AGENT_CONTAINER_NAME` (override container name), `AI_AGENT_HOST_ELAN=off` (use the `ai_agent_elan_home` volume instead of bind-mounting host `~/.elan`).
If `$SSH_AUTH_SOCK` is set on the host the wrapper forwards it automatically; verify with `ai-agent-jailed bash` then `ssh -T git@github.com`.
## Telling agents about your project (`CLAUDE.md` / `AGENTS.md`)
Both agents look for a project-specific instructions file at the repo root: **Claude reads `CLAUDE.md`**, **Codex reads `AGENTS.md`**. Commit one in your project so each session starts with your conventions in context. To keep a single source of truth, symlink one to the other:
```bash
ln -s AGENTS.md CLAUDE.md # or the other way around
```
Both agents read whichever file the symlink resolves to.
A starting block to paste into your `AGENTS.md` / `CLAUDE.md`, covering the things the agent has no way to infer from the repo because they come from the container, not the project:
````markdown
## Environment (provided by podman-ai-agent-isolation)
You are running inside a rootless Podman container with read-write access to
`/work` (this repo) and nothing else on the host. Use the tools listed below
in preference to writing one-off shell pipelines.
### Available CLI tools
`fd`, `rg`, `ast-grep`, `comby`, `difft`, `hyperfine`, `watchexec`, `delta`,
`yq`, `jq`, `scc`, `tree-sitter`, `entr`, `parallel`, `rga`, `dtrx`,
`shellcheck`, `sd`, `latexmk`, `biber`, `ott`, `gh` (with the `gh-sub-issue`
extension installed).
### MCP tools
- `lean-lsp` is pre-wired (via `uvx lean-lsp-mcp`). Use it to inspect Lean
goals, hover info, and diagnostics; do not grep `.olean` files or re-derive
goal state by hand.
<!-- Add other MCP servers you've configured here. -->
### Skills
The Claude Code `lean4-skills` plugin is loaded automatically; reach for its
skills (`prove`, `autoprove`, `review`, `golf`, …) when proving or
refactoring Lean. <!-- Add any extras from extra_skills in .ai-agent.json. -->
### Lean / Lake
The Elan toolchain pinned by `/work/lean-toolchain` is pre-installed. Use
`lake build`, `lake exe cache get`, and the Makefile targets normally.
**Do not run `lake clean`** unless the user explicitly asks: it wipes
`/work/.lake/build/`, which is bind-mounted into the host, invalidating the
Mathlib cache for both sides. After a clean you would need
`lake exe cache get` to refetch.
### Git and network
- `--network host` is on, so localhost services on the host are reachable.
- The host SSH agent is forwarded; `git fetch / pull / push` and `gh` work.
- **Do not `git commit` or `git push`** unless the user explicitly asks.
Use `git diff`, `git log`, `git status` freely.
- For `gh sub-issue add <parent> <child>` and any `gh issue create` /
`gh issue comment`, pass the body via `--body-file <path>` rather than
inline strings to avoid backtick / quoting problems.
- Always request user approval before opening, closing, or commenting on
GitHub issues / PRs.
````
Trim or extend to taste. When an agent gets the same thing wrong twice, the right fix is usually a sentence here, not another in-session correction.
## Updating Claude Code and Codex
The CLIs are baked into the image at build time. Auto-update is disabled inside the container — agents that complain about a stale version (`New version available…`) want you to rebuild the image.
```bash
./scripts/build-ai-agent-container
```
Every run cache-busts the Claude Code and Codex layers (`CLAUDE_UPDATE` / `CODEX_UPDATE` build args use the current Unix timestamp), so you always get the latest published versions without further flags.
What a rebuild preserves: everything in the `ai_agent_*` Podman volumes survives untouched — Claude / Codex auth, Codex session history, settings and MCP config (`ai_agent_config`), Lean/Lake/uv caches (`ai_agent_cache_*`), Elan toolchains (`ai_agent_elan_home` when not using the host bind-mount), SSH `known_hosts` (`ai_agent_ssh`), and the Codex skills dir (`ai_agent_skills`). Your project at `/work` is bind-mounted, so it is unaffected by anything in the image. Only what's inside the image itself (the CLI binaries, system packages, lean4-skills clone, baked extra skills) is replaced.
Old image layers from previous rebuilds pile up in podman storage and can eat tens of GB. Reclaim disk space periodically:
```bash
podman image prune # remove dangling (untagged) images
podman image prune -a # remove every image not used by an existing container
```
The `-a` form is more aggressive: it will also drop the previous `localhost/<project>-agent:latest` if podman has already retagged it, so be sure no other tag you care about lives only in podman storage.
## More
[`doc/design.md`](doc/design.md) covers the architecture: volume layout, entrypoint behaviour, security model, skills-baking pipeline, OCI label derivation, advanced rebuilding, and migration notes.
## Acknowledgements
Inspired by the ["localdev-container-jail"](https://blog.herlein.com/post/localdev-container-jail/) pattern.
