Liquid Types as a behavioural sandbox for agents

Current permissions in agents are inadequate and fail to prevent the lethal trifecta issue, according to this post. The most potent aspect of agents, which is also their weakness for critical applications, is their access to terminals, files, computers, and the internet. Every time you employ an agent for coding, you must grant permission for every terminal command it intends to execute.

This security measure is no longer effective, as research spanning decades has demonstrated. When security compromises user productivity, users resort to various tactics to reduce the barrier. Consequently, agents often appear harmless commands that you accept, and once the benefits of agents become limited by the need for babysitting, users switch to "dangerously-skip-permissions" or "yolo" mode, eliminating any constraints on permissions.

Data indicates that manual review can become a habit, with users approving 97% of permission prompts in Claude Code. While most prompts likely pertain to safe, routine commands, a permission approval rate of 97% suggests that many users are reflexively clicking through without reviewing each command. Although Anthropic and other companies have developed a compromise, employing an LLM to classify whether each external call should be allowed or result in a permission request, this guardian LLM is not guaranteed to always function correctly.

In fact, it shares the same training data and possibly similar architectural components with the agent, making it probable that it fails in the same situations where the agent LLM also generates incorrect commands. Therefore, we cannot entirely trust this guardrail system. This might be acceptable for developing personal websites but not for critical data such as healthcare, defense, or even simple sharing of proprietary data.

Most modern agents are susceptible to a type of attack known as the lethal trifecta. This attack surface emerges when three conditions coexist: your Claude agent has access to your GitHub account, containing both public and private repositories. You grant it permission to read information from repositories on the internet (open-source projects), your public repositories (to contribute to open-source), and your private repositories (to assist with your job).

However, when all these permissions are combined, it can search for something on the internet (which you cannot control), retrieve instructions to read from your private repository (since it has permission), and publish all the code in one of your public repositories. This scenario is not merely a hypothetical example; Microsoft leaked customer emails, and Claude Cowork exfiltrated files.

Microsoft Copilot Cowork also exfiltrated private information, and Supabase MCP exfiltrated all their database. Simon Willison has documented several such reports. The key takeaway is that our current guardrails are either highly granular (per-request permissions) or overly coarse (per-application/agent permissions). We require something more substantial.

We need behavioral permissions. Over the past eight years, I have been researching Liquid Types. The primary idea behind Liquid Types is to model additional information in the type system, not only rejecting programs that pass an integer where a string was expected but also allowing programs to use objects in invalid states. As Yaron Minsky suggested, "You should make invalid states unrepresentable" (as I found in my Google research).

I have developed three systems using Liquid Types (Aeon, LiquidJava, and ROSpec). For instance, if you call divide 4 0, you will receive a compiler error because divide only accepts a second argument different than 0. If you call let z = read_input in divide 4 z, the program will fail because read_input returns an integer, and there is no proof that it is different than zero.

Therefore, the program is rejected. Alternatively, you could do something like let z = read_input in if z = 0 then 0 else divide 4 z, which would work since on the 'else' branch, we know z to be different than 0, enabling us to construct a proof. Liquid Types is a type theory that allows us to write refinements on types and reason about programs.

Although Lean possesses greater expressive power (requiring explicit proof writing by the user or agent, consuming time and tokens), Liquid Types are deemed appropriate for guaranteeing safety in several systems without the additional proof generation cost. Liquid Types can detect bugs in a drone controller and identify 84 real-world ROS robotics misconfigurations.

In the data science domain, Liquid Types can uncover various conceptual errors, such as using classifiers under incorrect assumptions or data leakage issues. Agents' power is also their primary safety weakness: unlimited access to the terminal, your computer, and the internet. To address this, critical systems should have behavioral limitations on sandboxes.

I propose using a language with a flavor of dependent types (Liquid Types in this case) as a means of specifying guardrail policies. Aeonbox is an agent harness, similar to Codex or Claude Code, that interactively prompts users for a prompt and then executes it. However, Aeonbox lacks terminal access, only possessing the GitHub SDK written in Aeon with its safeguards.

The excerpt above is part of the GitHub API. The first line declares a function named divide that accepts two arguments.