Liquid Types proposed as compile-time guardrails for agent behaviour to block lethal trifecta attacks

The proposal replaces runtime permission prompts with compile-time Liquid Types that encode behavioural rules. Instead of asking a user to approve every terminal command, the compiler rejects any program that could violate a logical constraint, for example, an agent that might read a private repository and then publish its contents to a public one. This shifts the burden from human review to formal proof, eliminating the reflexive approval problem documented in Claude Code usage data.

Liquid Types refine standard types with logical predicates. A function that divides two integers can be annotated to accept only non-zero denominators; the compiler then rejects any call where the denominator might be zero. In the agent context, the same mechanism can express rules such as “no private data may be sent to an untrusted destination” or “no file write may follow an untrusted network read.” These rules are decidable, so the compiler either accepts the program or rejects it with a counter-example, removing the probabilistic uncertainty of LLM-based guardrails.

The cost of adoption is upfront proof construction. Developers must annotate types with the desired constraints and, in some cases, provide explicit proofs that the constraints hold. While this is less onerous than writing full proofs in a system like Lean, it still requires familiarity with refinement types and SMT solvers. The benefit is that once the types are in place, the compiler guarantees the constraints are never violated, even if the agent is later modified or extended.

Where the mechanism stops working is at the boundary of decidable logic. Liquid Types are intentionally restricted to decidable fragments of first-order logic, so they cannot express arbitrary properties. Complex policies that require temporal reasoning or higher-order quantification may still need runtime monitoring. Additionally, the approach assumes that the agent’s code is statically analysable; dynamically generated or interpreted code bypasses the compile-time checks entirely.