With AI agents rampaging on half the population’s computers, there is increased interest in safe-guarding AI agent workflows. In “Tracking Capabilities for Safer Agents” no one less than Martin Odersky (et al) propose a framework for running AI agents subject to security policies. The answer is – of course – Scala.
I’m skipping the problem description; if you’re reading this in 2026, you’re probably aware of the issue. If you’re reading this in the distant future: I’m glad we didn’t annihilate ourselves. Now on to the paper. The authors propose placing the agent in a programming language-based “safety harness.” Instead of issuing raw tool calls, the agent writes and submits code in a capability-safe language, specifically Scala 3 with “capture checking“. Capture checking is a new Scala feature which tracks the capabilities a piece of code holds on to in the type signature. Imagine permissions as types. Capture checking is transitive, so if a subroutine needs a capability, the caller needs it, too.
The runtime architecture “tacit” (Tracked Agent Capabilities In Types) is implemented as an MCP server and sits between the LLM and the host operating system, acting as a strict gateway. It consists of three main components:
1. The capability-safe library (API): this is a predefined set of Scala objects and methods (like FileSystem or DocBase). It serves as the only interface for interacting with the real world (files, network, running processes).
2. The Scala compiler (gatekeeper): when the agent submits code, it is first passed to the Scala compiler which checks the types and “capture sets” (capabilities used). It statically verifies that the code isn’t trying to leak data or use permissions it wasn’t given.
3. The Scala REPL (executor): if the code successfully compiles and passes all type checks, it is executed in a read-eval-print loop (REPL). The result is then returned to the agent.
With regard to information access, tacit implements the concept of “Local Purity & Information-Flow Security”. For example, highly sensitive data can be wrapped in a classified container. The only way the agent can process this data is by supplying a statically pure function (a function holding an empty capture set). Because a pure function has no side effects, it is mathematically verified by the compiler that the data cannot be leaked to the network or written to unauthorised files.
George's Techblog 