The Contract, Enforced Twice

I. No One Is Watching

The last essay described lex-lang's premise: a function's effects are part of its type, checked before the code runs. Declare net, and you can open a connection. Reach for io.write without declaring it, and the compiler refuses before a single line executes.

That is a real guarantee, and it has a real limit: a type checker only watches code written in its own language. It says nothing about a shell command the agent decides to run instead, a binary it downloads and executes, or a call that goes around the interpreter entirely. In most agent systems that gap doesn't matter much in practice, because a human is reading the output before it takes effect — approving the pull request, clicking "allow" on the tool call. The human is the second check.

lex-os is what happens when you remove that assumption on purpose. It's a runtime built for the case where an agent is handed a goal and a box and operates without anyone watching live, until the goal is met, the budget runs out, or it's stopped. No human in the loop means the compiler's word can't be the only word.

II. One Grant, Two Gates

Every lex-os run starts from a manifest: a goal, a grant (what filesystem, network, and exec access is allowed), a budget (wall-clock time, command count, money, API calls), and an isolation floor. The grant is one value. It drives two independent enforcement paths, not one.

The first layer is the one from the last essay: lex-os check runs the agent's .lex program through the real Lex compiler front end and refuses to let it run if its declared effects exceed the grant. That's a compile-time question with a compile-time answer.

The second layer doesn't ask what language produced the command. lex-os-perimeter takes the same grant and derives a sandbox policy from it — in production, a real Firecracker microVM behind a host-side network wall. It enforces at the kernel and hypervisor boundary, which means it holds even for an agent that never touches the Lex compiler at all: a raw shell command, a downloaded binary, anything the box can execute. The perimeter doesn't read source code. It watches what actually crosses the edge.

III. What Refusal Looks Like

Here is the first gate, live. A grant allows filesystem access but no network:

{
  "grant": { "filesystem": "ReadWrite", "network": "None", "exec": "None" }
}

And a program whose one real job is to submit a report over the network it wasn't granted:

fn submit(report :: Str) -> [net] Result[Str, Str] {
  net.get("https://results.demo.internal/submit")
}

Type-checking that program against that grant fails before anything runs:

$ lex-os check --grant analyze.json submit_report.lex
Error [PRECONDITION_FAILED]: grant violation: effect `net` needs
  network ≥ `allowlist` but the grant only provides `none`
exit 8

That's the compiler doing its job. Now the second gate, on a different question entirely: not "does this program's declared effects fit the grant," but "can this host actually provide what the manifest demands." A manifest that asks for the strongest isolation floor, resolved against a host that can only offer the weakest:

$ lex-os resolve --manifest sudo-dangerous.json --namespaces-only
Error [PRECONDITION_FAILED]: environment cannot satisfy manifest: needs
  isolation floor `microvm` but host tops out at `namespace` —
  refusing to downgrade
exit 8

Neither refusal is a fallback or a warning. Both are hard stops, and both say exactly what was missing — which matters when the thing reading the error is another agent, not a person scrolling a log.

IV. Refuse, Don't Downgrade

That resolver error is one instance of a rule that shows up in three unrelated parts of lex-os, independently: when the environment can't satisfy the manifest, when the real microVM perimeter isn't available and you haven't explicitly asked for the weaker simulated one, and when a third-party package wants more than it's been given. In every case, the answer to "we can't give you what was declared" is a refusal that names the gap — never a quiet run at reduced strength.

The third case is the interesting one, because it turns the same mechanism that stops an agent from escalating its own privileges into a supply-chain control. A distributable package — a capsule — travels with a signed declaration of the grant it needs. Installing it takes the intersection of what the consumer is willing to give and what the publisher says it needs:

consumer grant:  filesystem=ReadWrite  network=Allowlist[api.acme-pdf.com, *.finance.internal]
package needs:   filesystem=ReadOnly   network=Allowlist[api.acme-pdf.com]

installed at:    filesystem=ReadOnly   network=Allowlist[api.acme-pdf.com]

The package runs at the narrower of the two, every time — not the publisher's word taken on faith, and not the consumer's full grant handed over because the intersection was tedious to compute. It's the same narrowing check, applied twice: once to stop an agent from proposing a wider grant for itself mid-task, and once to stop a package it installs from getting more than the agent itself was trusted with.

V. The Log That Can't Be Edited

Every mediation decision is written to a hash-chained audit log before the box does anything else. There's no edit or truncate function anywhere in the audit crate — an agent tampering with its own history isn't prevented by a permission check, because the operation to do it doesn't exist to call.

Running the built-in demo shows what that buys you. The agent reads files, deliberately destroys its own box mid-task, and gets rebuilt by the supervisor from the manifest and the last checkpoint — recovery driven entirely from outside the box, by something the agent inside it can't reach:

{
  "outcome": "GoalMet",
  "reprovisions": 1,
  "audit_entries": 22,
  "audit_verified": true,
  "security_boundary": false
}

security_boundary: false is the simulated perimeter being honest about itself — it runs anywhere for tests and demos, but it is not the real wall. The real one is a microVM. What's constant across both is the audit trail: because nobody reviewed this session as it happened, the record has to be trustworthy after the fact by construction, not by anyone's discipline about writing things down.

VI. Where It Sits

lex-os sits on top of lex-lang and pulls its trust lattice directly from it — the same Grant type drives the compiler's type check and the runtime's sandbox policy because it's one definition, not two that happen to agree today. It's an honest proof of concept, not a finished product: one box at a time, no multi-tenant scheduling yet, and the isolation backends are namespaces or a real microVM — nothing in between shipped so far.

What's stable is the shape of the answer to "how do you trust an agent operating without supervision": not a more careful prompt, and not a human checking every action, but a single declaration enforced by more than one thing that doesn't trust the other to have caught it.

Open source under EUPL-1.2, EU-built. The source and the full demo — including the three-walls walkthrough above — are at github.com/alpibrusl/lex-os.

VII. Where People Push Back

"Both walls derive from the same Grant value — isn't that a single point of failure? A wrong grant breaks both layers identically." Yes, and this is the real residual risk, not a gap I want to gloss over. The redundancy protects against an independent implementation bug in the compiler or the perimeter — one enforcing the grant wrong while the other still catches it. It does not protect against the grant itself being wrong: if the manifest is too permissive, both layers will faithfully enforce a boundary that's in the wrong place. That's still a judgment call for whoever writes the goal and grant, and no amount of enforcement machinery substitutes for it.

"'Refuse, don't downgrade' sounds nice in a demo — doesn't it make the system unusable whenever a KVM host isn't available?" That's the tradeoff, deliberately. The alternative is an agent that believes it's inside a microVM when it's actually in a weaker namespace jail, with nothing telling it — or you — that the boundary quietly got thinner. In practice it means you provision hosts that satisfy the isolation floor you're declaring, rather than declaring an aspiration and hoping the runtime figures it out. Inconvenient by design; a silent downgrade would be worse, because you wouldn't know to compensate for it.

"It's an 'honest proof of concept' — one box at a time, no multi-tenant scheduling. How far is this from something real?" Far enough that it's worth saying directly rather than letting the architecture talk imply otherwise. The mechanism — one grant, two independently-enforcing paths — doesn't need multi-tenancy to be real or tested, and it is. Running many boxes concurrently at scale, with contention for host resources, is genuinely unbuilt.

"If no human is watching live, how do you ever catch an action that's within the granted scope but still wrong — the agent deletes the correct-looking but wrong row?" You don't, not with this mechanism. The grant bounds categories of harm — which paths, which hosts, how much money — not the correctness of an action taken inside those bounds. Reversibility classing and the audit trail exist for exactly this gap: an irreversible-consequential command refuses by construction regardless of the grant, and everything else is bounded and reviewable after the fact rather than prevented outright. Bounding the blast radius is not the same claim as catching every mistake.

"The audit log is 'tamper-evident' — to whom? What stops someone with root from just deleting the file and starting a new chain?" Nothing does, and that's a real limit, not an oversight. Hash-chaining detects reordering, deletion, or an edited payload within an existing log — audit verify walks the chain and would catch a broken link — but nothing forces anyone to run it, and no cryptographic scheme stops an operator with root from discarding the whole log and starting fresh. This designs out silent tampering of a log that exists; it doesn't design out someone choosing not to look, or destroying the evidence outright. That's a governance question, not a technical one this repo answers.

"Isn't 'enforced twice' just theater if a hypervisor escape defeats both walls in one move?" Yes, on the failure mode that matters most. The two layers are independent with respect to bugs in how each one translates the grant into policy — a compiler bug and a perimeter bug are two different pieces of code making two different mistakes. They are not independent with respect to a genuine Firecracker or KVM vulnerability, since the type check only ever ran before the box existed and has nothing left to say once it's running. That's why the perimeter being a narrowly-scoped, widely-audited microVM implementation — rather than something built in-house — matters more than the two-layer story does on its own.

— Alfonso Sastre, August 1, 2026