Ask a coding agent to add a task, and the diff fills up with shell commands. Few people review them down to what npm install runs underneath.
What can those commands overwrite, and what can they talk to? I wanted a machine to answer that before anything runs.
I build Lask, a task runner where you write tasks as typed functions in a small language, and every command runs in a container of the Docker image you declared for it.
Lask 0.15.0 adds within: you declare which files and networks commands may access, and the type checker verifies it statically.
This post has two parts. The first part steps away from Lask and summarizes the recent discussion about guardrails for generative AI. I tried to keep it objective, and I mark where I give my own opinion. The second part shows how I implemented those ideas in Lask, so it is mostly my own take.
TL;DR
Part 1 (general)
-
Reading code was never a strong defense against malicious code, and with AI producing more code, review is falling further behind.
-
One response is to have AI prove its code correct. But proofs need a specification written by a human, which doesn't fit things like the install scripts
npm installruns.- Another response, with growing research behind it, is to verify the boundary around the model, which holds whatever the model outputs. Part 2 (Lask) -
Lask's
withinimplements that second idea as type checking in a task runner. Commands that might exceed the declared scope faillask checkbefore anything runs.- I suggest a split: a person checks the access scope withlask envs accessbefore running, andlask checkverifies that every command stays within it. This is static checking, not a machine-checked proof, and there are things it doesn't cover. They're listed near the end.
Even when people wrote all the code, finding malicious code by reading it was hard.
The xz Utils backdoor, found in March 2024, wasn't caught by reading code (XZ Utils backdoor). Andres Freund, a PostgreSQL developer, traced it while investigating unusually high CPU usage during SSH logins.
Dependency code often isn't read at all. Imtiaz and Williams studied updates to popular packages in four package registries (arXiv:2206.09422). 52.5% of updates were only partially code-reviewed, and only 9.0% of packages had every update fully reviewed.
The report from the S3C2 industry summit on supply chain security reaches the same view (arXiv:2505.10538). Since there is no reliable automated way to detect malicious commits, teams rely on human review, but human review is error-prone and not always reliable.
With AI writing code, there's more for people to read.
Chen and Stratton at Harvard analyzed development data from 655 firms (Artificial Intelligence in the Firm). It's a working paper estimating how AI coding tools affect development, and it hasn't been peer-reviewed. After firms adopted AI agents, lines of code added rose 44.0% and pull requests opened rose 35.7%. Meanwhile, the average time from opening a pull request to merging it grew 56.1%. The authors conclude that code review became the bottleneck.
He et al. followed 802 developers at a company that mandated doubling output with AI (arXiv:2607.01904). Load per reviewer roughly doubled.
Reading code was already a weak defense against malicious code, and AI leaves even less room to read. So I think we need checks that a machine can do without a person reading the code.
In December 2025, Martin Kleppmann predicted that AI will make formal verification mainstream (AI will make formal verification go mainstream). Formal verification proves mathematically that a program meets its specification. His argument: AI makes writing proofs much cheaper, so instead of having people review AI-written code, have the AI prove it correct.
With this approach, it doesn't matter if the AI writes a bad proof. The proof checker rejects it and makes the AI try again.
But in the same post, Kleppmann notes that reading and writing formal specifications still takes expertise and careful thought. A proof only guarantees that the code meets the spec, and a person writes the spec.
I think proof-based verification is hard to apply to tasks like builds and installs. npm install runs install scripts written by other people, one for each dependency that has one. Nowhere is there a spec for what those scripts should do.
This year, those install scripts were exactly what attackers used on npm. Palo Alto Networks' Unit 42 updated its overview of attacks on npm on July 15, 2026 (The npm Threat Landscape). It says many compromises rely on preinstall or postinstall hooks to exfiltrate secrets.
According to the same article, in the May TanStack incident, code injected into CI harvested NPM_TOKEN and GITHUB_TOKEN. In April, a self-propagating worm was reported that used stolen npm tokens to publish versions carrying malicious code (The Hacker News).
The common advice is ignore-scripts, which stops install scripts. But some packages need their scripts, so stopping all of them isn't always practical.
Instead of checking that AI output is correct, a growing body of research checks the boundary that AI output can't cross, whatever it is.
Moon and Varshney's Containment Verification (arXiv:2605.09045) assumes nothing about how the AI behaves. It treats the AI as able to emit any value within the types the framework accepts. It then proves in Dafny that the agent framework enforces its boundary policy for every such value. The authors say the guarantee doesn't depend on alignment, that is, on whether the model has been tuned to behave as intended.
Google DeepMind's CaMeL (arXiv:2503.18813) also leaves the model untouched. It places an interpreter outside the model that records where each value came from and checks those records against a policy before any tool call, to defend against prompt injection.
Anthropic's Agent SDK documentation draws the same line between permission checks and isolation (Securely deploying AI agents). Of the mechanism that parses commands and matches them against permission rules, it says: "This is a permission gate, not a sandbox."
Putting this together, the mechanisms that guard against an agent's risky operations fall into three layers. Each works at a different time and checks something different. Table 1 lists them in the order they act.
Table 1. Three layers against risky operations
| Layer | What it checks | When | If it gets it wrong |
|---|---|---|---|
| Static boundary check | Whether the isolation mechanism and its settings keep to the decided scope | Before running | It runs with isolation that doesn't keep to the scope |
| Permission check | Whether this operation may run | Right before running | The operation runs |
| Runtime isolation | What a running operation can access | While running | It accesses more than intended |
A static boundary check examines the isolation mechanism, such as a container or sandbox, and its settings before anything runs. Containment Verification, from the previous section, proves that the framework enforces its boundary policy whatever values the AI emits. It checks the isolation, not the AI's output, so the result doesn't change whatever the AI writes.
A permission check decides, right before running, whether an operation runs. Permission rules and confirmation prompts belong here. If the check gets it wrong, the operation simply runs.
Runtime isolation has no say in whether something runs. The operation runs, but it can only access what's inside the isolation. Even a risky operation that got past the permission check is contained. But if the isolation is configured too broadly by mistake, it can access more than intended. Without a static check, nobody usually verifies those settings until something runs.
The three layers are meant to be stacked. The static check catches mistakes in the isolation settings before anything runs, and isolation contains risky operations that got past the permission check.
From here on, it's about Lask. I implemented the static boundary check, the first layer in Table 1, as type checking in a task runner.
Lask has always run every command in a container. The host's home directory and ~/.ssh aren't visible from inside.
But it mounted the repository directory read-write at /work. An install script could overwrite source files, read .env, and talk to the outside world.
With base_access, you can narrow that mount path by path. The example below makes the whole repository read-only, lets only dist be written, and makes .env appear empty. network: "none" also cuts off outside access.
offline = #node:24.21.0-alpine3.24{base_access: { ".": "ro", "dist": "rw", ".env": "none" }, network: "none"}
In a container with these settings, I tried writing to the source, reading .env, and reaching the npm registry.
$ touch src/x.js
touch: src/x.js: Read-only file system
$ wc -c .env
0 .env
$ node -e "fetch('https://registry.npmjs.org')..."
TypeError: fetch failed
[cause]: Error: getaddrinfo EAI_AGAIN registry.npmjs.org
.env is 11 bytes on the host but 0 bytes inside the container. I checked this with Lask 0.15.0, Docker Engine 29.5.3, and macOS 26.6.2 on Apple Silicon.
So far, you could do the same by assembling Docker's --mount and --network none yourself. The difference is the check in the next section.
within declares what a module or function may access. Written at the top of a module, it covers every declaration in the module.
// main.lask
within { files: { ".": "ro", "dist": "rw", ".env": "none" }, network: "none", volumes: false, publish: false }
offline = #node:24.21.0-alpine3.24{base_access: { ".": "ro", "dist": "rw", ".env": "none" }, network: "none"}
// Builds into dist without any network.
build(): String = do {
$[offline] npm run build
read_file("dist/manifest.json", offline)
}
It can restrict four things:
files: what can be read or written, path by path, inside the repositoryvolumes: whether host paths outside the repository can be mounted network: whether the container can talk to the outside publish: whether the outside can connect to the container
lask check follows every place in the module that runs a command, and verifies that the settings of the container running it stay within the declaration.
Now suppose an agent adds a task that uploads dist to a preview server. It needs the network, so the agent also adds within { network: "default" } to the function.
// main.lask (added)
// Uploads dist to the preview server.
upload() within { network: "default" } = do {
online = #node:24.21.0-alpine3.24{base_access: { ".": "ro", "dist": "rw", ".env": "none" }}
$[online] npx -y some-up dist
}
Here's what lask check says:
$ lask check
main.lask:14:3-14:38: E-TYPE-WITHIN-EXCEEDED [static]: the network is "default", which within { files: { ".": "ro", ".env": "none", "dist": "rw" }, volumes: false, network: "none", publish: false } of the module does not allow (network)
note: the constraint is at main.lask:1
note: reached through upload, at main.lask:14
The module's within acts as a ceiling, so a function's within can't widen it. A function's constraint is checked together with the module's, and both must hold.
lask run runs the same check first, so not a single task in this module runs.
If a network setting is read from an environment variable, its value isn't known until the program runs. Lask treats that as "can't be shown to hold" and reports an error.
within { network: "none" }
probe(): String =
$[runnable(#node:24.21.0-alpine3.24, network = get_env("NET"))] node --version
bash
$ lask check
p.lask:4:3-4:81: E-TYPE-WITHIN-UNPROVEN [static]: 'network' is not known here without running the program, so within { network: "none" } of the module cannot be shown to hold
E-TYPE-WITHIN-EXCEEDED means the scope is shown to be exceeded. E-TYPE-WITHIN-UNPROVEN means it couldn't be shown not to be. To pass, settings that affect the scope must be literals or names bound to literals. That's less convenient, but once you declare a constraint, I decided only what is shown to stay within it should pass.
When a function takes an image and its settings as an argument (an "environment" in Lask), the check happens at each call site. For a function you invoke directly with lask run, it uses the arguments from the command line and checks before running.
#local, which runs commands directly on the host, can access the whole host, so it satisfies no constraint.
l.lask:3:20-3:38: E-TYPE-WITHIN-EXCEEDED [static]: #local reaches the whole host, which within { network: "none" } of the module does not allow (network)
Installing dependencies needs the network. So I put installation in a separate module that allows network access but can only write node_modules.
// deps.lask
within { files: { ".": "ro", "node_modules": "rw", ".env": "none" }, volumes: false, publish: false }
deps = #node:24.21.0-alpine3.24{base_access: { ".": "ro", "node_modules": "rw", ".env": "none" }}
// Installs dependencies; install scripts can reach the network but write only node_modules.
export install() = $[deps] npm install --no-package-lock
Install scripts can reach the outside, but they can't read .env or overwrite source files. The build side can read node_modules but can't reach the network.
Figure 1. What each task's container can access
lask envs access lists what the commands in a module can access. It runs nothing and doesn't contact the container engine.
$ lask envs access --module deps.lask
ENVIRONMENT FILES NETWORK CHECK REQUIRED BY
#node:24.21.0-alpine3.24{base_access} . ro, .env none, node_modules rw default ! ok deps.lask: install
1 row (1 registry): 1 ok
! marks anything that can access beyond the repository. Here, it shows that the container can reach the outside.
In Kleppmann's argument, people read the spec and a proof checker verifies that the code meets it. I think Lask can narrow what people read in the same way. Instead of reading every command an agent added, you check the access scope with lask envs access before running.
$ lask envs access build
within { files: { ".": "ro", ".env": "none", "dist": "rw" }, volumes: false, network: "none", publish: false }
ENVIRONMENT FILES NETWORK CHECK REQUIRED BY
#node:24.21.0-alpine3.24{base_access,network} . ro, .env none, dist rw none ok main.lask: build
1 row (1 registry): 1 ok
Given a function, the first line shows the constraint the function is checked against. Below it are the scopes of the commands the function runs.
The list is built from the same code that runs. If an agent edits the within line itself, the constraint on the first line changes, so you notice before running.
Without a function, you get the list for the whole module. With the upload() task from earlier, it looks like this:
$ lask envs access
ENVIRONMENT FILES NETWORK CHECK REQUIRED BY
#node:24.21.0-alpine3.24{base_access,network} . ro, .env none, dist rw none ok main.lask: build
#node:24.21.0-alpine3.24{base_access} . ro, .env none, dist rw default ! exceeded main.lask: upload
2 rows (2 registry): 1 ok, 1 exceeded
An exceeded row is a task with a command that goes beyond the declaration. Rows marked ! tell you which tasks talk to the outside. envs access runs nothing, and it exits with 0 even when something exceeds the scope.
A person reads this list, and lask check verifies that every command stays within it. However many tasks an agent adds, this list is all a person needs to check.
The split looks like this:
lask envs access. lask run checks the module before running anything.ok, the commands run. If anything is exceeded or unproven, nothing runs.
within is a static check done by Lask's type checker. Unlike Containment Verification in Part 1, the checker itself isn't machine-verified, for example in Dafny. If the checker has a bug, a command that exceeds the scope can still pass.
What it protects is limited too:
none or default. The install scripts in deps.lask can talk to anywhere on the internet. The next section covers limiting destinations.env can be read by that command. Pass a secret to a container with network access, and it could still be exfiltrated.#local satisfy no constraint. Tasks that need within. lask sync, which builds and pulls images, isn't covered. npm install directly from a shell, Lask can't check it.
The last point is a separate problem: how to restrict the agent's own permissions. That belongs to the agent's permission settings and sandbox.
Outbound traffic from containers (egress) is currently all or nothing. The npm install in deps.lask only needs to reach the npm registry, but with network: "default", install scripts can reach anywhere on the internet. As with the npm worms in Part 1, any secret they can read could be sent out.
So, as the next step, I'm considering egress that lets you list the destinations a task may reach. The design I have in mind:
The task's container has no way out except through the proxy, so an install script that tries to bypass the proxy can't reach the outside. This is still at the design stage, and the syntax isn't decided.
It's getting hard to read all the code AI writes. But you can narrow what people read to the list lask envs access prints, and leave the rest to type checking. That's what I wanted to show in this post.
within just landed in 0.15.0, and both how constraints are written and what the check covers are still being worked out. I'd love to hear how it works for you, or what constraints you'd want.