The Contract Your Agent Signs

I. The Implicit Trust

When you hand a piece of code to an agent and ask it to execute, you are making a trust decision. You may not think of it that way — it looks like a function call, a tool invocation, a step in a pipeline — but underneath, you are granting that code access to everything the process can reach: the filesystem, the network, the environment, the other services your credentials can talk to.

The trust is total and it is invisible. The code does not say what it needs. The runtime does not check what it uses. If the agent generates something that reads /etc/passwd on the way to doing something else, nothing stops it. If a tool that was supposed to fetch a URL also writes a file, nothing catches that. You find out afterwards, if you find out at all.

This is not a niche problem. It is the default condition of every agent system built on top of conventional programming languages — which is to say, almost all of them.

II. Effects as the Contract

Lex-lang starts from a different premise: a function's effects are part of its type. Not documentation. Not a comment. The type. When you write a function in Lex, you declare what it is allowed to do — read files, open a network connection, write to a database — and that declaration is checked before the code runs.

This is what a typed-effect language means in practice. The question "what is this code allowed to do?" has a machine-checkable answer, encoded in the type of every function in the program. You don't have to read the implementation to know. You don't have to trust the author. You read the type.

III. What the Rejection Looks Like

Here is a concrete example. An agent is given a tool that is supposed to fetch a URL. The tool is granted the net effect — network access. Somewhere in what the agent generated, it also tries to read from the local filesystem:

lex agent-tool --allow-effects net --input "url" \
  --body 'fetch(url) |> then(io.write("/tmp/cache", _))'

The type checker sees that io.write requires the io effect, which was not granted. The check fails before any code runs:

TYPE-CHECK REJECTED
  effect `io` not in grant [net]
  at: io.write("/tmp/cache", _)
  exit 2

No exception handler. No sandbox escape. No audit log to dig through after something went wrong. The rejection is the answer, and it arrives before execution.

This is the property the manifesto called "trust by verification, not comprehension." You do not need to understand what the agent generated. You need to know whether it fits the contract — and the type checker knows.

IV. Built for LLM Authorship

Most typed-effect systems were designed for human authors: expressive, annotation-heavy, with inference engines that reduce the burden of writing the types out. Lex-lang takes a different position. The primary author of Lex code is not a human — it is an LLM. The design reflects that.

Effect annotations are explicit and local. An LLM does not carry a mental model of an inference algorithm; it generates tokens. Explicit annotations mean the type is readable in the text the model produces, not reconstructed from what the compiler decided. A model that generates a function with the wrong effects gets immediate, local feedback: this specific annotation is wrong, here is why. That is the kind of error that survives being fed back into the context window.

The AST is content-addressed. Every expression has a stable hash derived from its structure, not from its position in a file. This matters because LLMs do not think in line numbers. A content-addressed representation makes it possible to talk about a specific expression — compare it, version it, attest to it — without anchoring to a coordinate system designed for human editors.

A language that treats line numbers as the primary identity of code is a language designed for the human who reads diffs. Lex is designed for the agent that reasons about structure.

V. The Attestation Graph

Effect checking tells you what a piece of code is allowed to do before it runs. The attestation graph tells you what actually happened after it ran — and who vouched for it.

Every artifact in a Lex program — every function, every module, every output — carries an attestation: a record of what produced it, what verified it, and what the verification said. Attestations are chained: the attestation on a deployed artifact traces back through the checks that cleared it, to the spec it was generated against, to the goal that produced the spec.

This is not logging. Logs record events; attestations record provenance. The difference matters when you want to ask not "what happened?" but "can I trust this?" — a question that requires knowing not just the history but the chain of verification that stands behind it.

In an agent system where code is generated at high speed by models you do not fully control, provenance is load-bearing. You are not reviewing every function. You are trusting the chain.

VI. Where It Sits

Lex-lang is the foundation of the Lex stack. Everything built on it inherits the same property: effects declared, checked, enforced. The stack so far:

• lex-os — the capability runtime for agents: a sealed, disposable execution environment where one trust grant drives both the type check and the sandbox.
• lex-loom — the cross-org agent fabric: runs work the way a company runs, with agents in the seats, evidence-gated handoffs, and an append-only trail as memory.
• lex-soft — B2B integration where the trust between agents across org boundaries is mechanical, not social: typed contracts, not invoices and disputes.
• lex-robot — the safety envelope for robotics: comprehension of a learned policy is impossible, so you bound it instead — capability grants before any command reaches hardware.
• lex-games — agent benchmarks where a submission is a trail, not a score: cheat-resistant by the same attestation logic that makes production code trustworthy.

All open source under EUPL-1.2, EU-built. Early in places, and openly a work in progress.

The design is not finished. The inference story will improve; the tooling is still sparse; some of the effect boundaries will move as we learn from building on top of them. What is stable is the premise: that the right response to code you don't fully trust is not more careful review — it is a type system that makes trust checkable, and a runtime that enforces the check.

If you are building agent systems and have wondered what it would look like to bound what an agent is allowed to do at the type level, rather than hoping the sandbox catches what you missed — Lex is the answer we are building. The source is at github.com/alpibrusl/lex-lang.

VII. Where People Push Back

"Effect systems aren't new — Koka, Frank, OCaml's algebraic effects have done this for years. What's actually new here?" The type-theoretic idea isn't new. What's new is the audience: these systems were built for a human author who benefits from inference doing the work quietly. Lex is built for an LLM author, so it makes the opposite bet — explicit and local over inferred and global — and it wires the same declaration into a runtime that enforces it again outside the compiler (see the follow-up on lex-os). The novelty is the pairing, not the type theory.

"An effect an agent legitimately needs can still be misused inside that scope — granting fs doesn't stop it from overwriting the wrong file. Doesn't this just move the trust problem?" Yes, and it's worth saying plainly: effect types answer "is this within the boundary that was declared," not "is this the right action." They narrow what a mistake can reach; they do not evaluate whether an in-scope action was a good idea. That's a real limit, not a rounding error — it's why the boundary needs to be drawn tightly, and why lex-os pairs it with reversibility classing so an irreversible, consequential command is refused by construction regardless of what the grant allows.

"Who checks the type checker? A bug in effect inference is a hole in the whole premise." Correct — the compiler is part of the trust boundary now, so its own correctness carries more weight than in a typical language. It hasn't been formally verified. It is adversarially tested: there's a dedicated fuzz target and test suite for effect soundness specifically (fuzz/fuzz_targets/effect_soundness.rs, crates/lex-types/tests/effect_soundness.rs), run against the checker on a schedule. That's evidence, not proof.

"What about code that isn't written in Lex at all — a shell-out, an FFI call, a downloaded binary?" The type checker only ever sees Lex source. That gap is real, and it's exactly what motivated the second half of this architecture: the same grant that the compiler checks is handed to a runtime that enforces it again at the kernel boundary, for anything the box can execute — not just code that went through the compiler. Covered in the next essay.

"The attestation graph — isn't that just logging with extra vocabulary? What stops someone forging the chain?" An attestation records what produced something, what verified it, and what the verification concluded — it answers "can I trust this without re-deriving it myself," not "can no one have lied." It isn't, by itself, cryptographically tamper-evident the way a hash-chained log is; that stronger property exists elsewhere in the stack (lex-os's audit log, capsule signatures), not in the attestation graph as described here. Worth being precise about which claim is which.

"Doesn't declaring every effect just add busywork for whoever writes the code?" For a human, probably. For an LLM generating tokens, the friction is closer to a compile error than an inspection burden — it's immediate, local, and specific enough to fix from within the same context window that produced the mistake. The cost is real; it's paid at the moment it's cheapest to pay.

— Alfonso Sastre, July 29, 2026