Five Bugs the Claim Layer Caught Before I Wrote Them

The claim layer shipped ten days ago. I've been using it on a real project since — not the demo payments app from the manual, but actual code with dependencies, third-party libraries, and an AI agent that writes most of the implementation. This post is not about what the claims are (the manual covers that). It's about what they catch — five concrete moments where a claim stopped a bug that would otherwise have reached production, each in a different way. The point is not "claims are theoretically nice." The point is: here are the five diffs I did not have to debug at 2 AM.

1. The dependency that started reading files

A JSON library. I'd been using jsonlib for six months — it parses bytes into a tree, nothing more. My Build.sj said:

static final String[] capabilities = {
    "myapp",       "net, fs.read",
    "jsonlib",     "",
};

jsonlib held no grants. Pure on purpose. Then I bumped the dependency from 0.3.2 to 0.4.0 — a patch bump, semver-compatible, changelog said "added schema validation." The build stopped:

error[E_CAP_DENIED]: package `jsonlib` performs `fs.read`
(native sj_FileInputStream_open) but holds no `fs.read` grant.
Grants for jsonlib: (none). Add "jsonlib", "fs.read" to Build.sj
capabilities, or remove the call.

Schema validation — by loading schemas from the filesystem. A JSON library that reads files. The claim layer turned a silent behavioral change into a one-line review question: do I want my JSON parser touching the filesystem? I didn't. I pinned to 0.3.2 and opened an issue with the library author. The bug it caught was not in my code — it was in someone else's, arriving through a dependency bump that looked routine.

Without the claim: the library reads files at runtime, in production, and I find out when a customer's security audit asks why a JSON parser has filesystem access.

2. The AI agent that wired telemetry into the domain layer

I asked an AI agent to add request logging to the payment service. The agent did what agents do: it found the most central place every request passes through and added the logging there. That place was payments.model.Ledger — the pure domain core.

package payments.model;

import sj.net.UnixGateway;   // <- the agent added this

public class Ledger {
    public long transfer(Account from, Account to, long cents)
        requires cents > 0
        ensures  result == cents
    {
        UnixGateway.send("logs", ...);   // <- and this
        ...
    }
}

Two claims caught it, in sequence, at compile time:

error[E_ARCH_DENIED]: package `payments.model` imports `sj.net`
but its architecture entry allows only: (none).

error[E_CAP_DENIED]: package `payments.model` performs `net`
but holds no `net` grant.

The architecture declaration said payments.model imports nothing — not even the network package. And the capabilities declaration said the model package holds no grants. The agent's output was dead on arrival. I didn't review the diff and notice a suspicious import — the compiler refused to build it.

The fix was the one the agent should have made in the first place: log from payments.app, the edge package that already holds net. One conversation with the agent, pointing it at the E_ARCH_DENIED message, and it got it right. Total time: 30 seconds. The claim layer gave the agent a named signal to fix, not a code review to interpret.

Without the claim: the domain layer now has a network dependency, every test of the domain logic needs a network mock, and the "pure core" is pure in name only.

3. The off-by-one that passed every test

A ledger withdrawal. The contract:

public long withdraw(long cents)
    requires cents > 0
    requires cents <= this.balanceCents()
    ensures  result == cents
    invariant balance >= 0
{
    balance = balance - cents;
    return cents;
}

Eight unit tests, all green. Then a refactor — someone (the agent, as it happens) changed the body to deduct a fee:

    balance = balance - cents - 1;   // $0.01 fee
    return cents;

The tests still passed — none of them happened to withdraw the full balance. But superj run threw:

ContractViolation: invariant balance >= 0
  at payments.model.Ledger.withdraw (Ledger.sj:42)

The test that triggers it: withdraw the full balance. The balance goes to -1. The invariant catches it. Not a test I wrote — the contract wrote it, by asserting a property that must hold for every exit, not just the ones my tests happened to cover.

The ensures result == cents also caught something subtler: a later change tried to return cents - 1 (the fee deducted from the returned amount instead of the balance). The ensures fired. The business rule — "you withdraw what you asked for" — is now a compile-time-checked runtime invariant, not a comment.

Without the claim: the off-by-one lives in production until a customer withdraws their full balance and gets a negative-balance error, or worse, doesn't get an error at all.

4. The allocation that crept into the hot path

A SEDA event handler. The steady-state path: receive a ping, publish a pong. I'd marked it noalloc to pin the entire call tree:

public noalloc void onPing(EventHeader header, Ping evt) {
    Pong pong = this.publisher.getHandler(Msgs.PONG).prepare();
    pong.msg = evt.ts;
    this.publisher.publish(Pong.SIZE);
}

Then the agent added a debug log line — only when a flag was set, only for development:

public noalloc void onPing(EventHeader header, Ping evt) {
    if (this.debug) {
        String msg = "ping " + evt.ts;   // <- string concatenation
        System.out.println(msg);
    }
    ...
}

error[E_NOALLOC] at the string concatenation. String + allocates. The noalloc modifier is transitive — it pins the whole call tree — so the allocation three lines into the method is caught at compile time. No runtime profiling, no flame graph, no "why did latency regress by 400ns after the last merge." The compiler said no.

The fix: move the debug log to a separate, non-noalloc method that the hot path calls only when debug is true. The noalloc on the steady-state entry point still holds; the debug path is free to allocate. That's the shape noalloc is designed to produce — the allocation boundary is explicit, not accidental.

Without the claim: the debug log ships to production behind a flag that someone forgets to turn off, the steady-state path allocates a String per event, and the SEDA latency budget silently degrades. You find it in a benchmark three weeks later and spend a day bisecting.

5. The import that broke the layering

A trading system. Three layers:

static final String[] architecture = {
    "trading.model",  "",
    "trading.risk",   "trading.model",
    "trading.exec",   "trading.model, trading.risk, httpkit",
};

Model is pure. Risk depends on model. Exec depends on both and talks to the exchange. One day, a change in trading.risk needed a price from the exchange's HTTP API. The agent added:

package trading.risk;

import sj.http.HttpClient;   // <- exec-layer concern

error[E_ARCH_DENIED]: package `trading.risk` imports `sj.http`
but its architecture entry allows only: trading.model.

The architecture declaration is a compile-time wall. trading.risk cannot import the HTTP client — not because the import is wrong, but because the layer it lives in is not allowed to talk to the network. The price lookup belongs in trading.exec, which holds net, with the result passed up to trading.risk as a parameter.

This is the one that would have been the most expensive to find without claims. The code compiles. The tests pass. The HTTP call works. But trading.risk now has a hidden dependency on the network, which means every risk calculation needs a live exchange to test, the risk module can't be reused in an offline backtester, and the clean layering that made the system comprehensible is gone — silently, in one import.

The fix: the agent moved the HTTP call to trading.exec and passed the price as a parameter. Two minutes, guided by the E_ARCH_DENIED message. The architecture stayed clean because the compiler enforced it, not because the team had discipline.

The pattern

Five bugs. Five different claims. One thing in common: each was caught at compile time or in a checked build, named with a stable diagnostic code, and fixed by a small change guided by the message. None required a code review to find. None required a test that someone had to think to write. None reached production.

The claims are not a verification system — they don't prove your code correct. They are a tripwire system: they state your intention in a thin layer, and the compiler holds every line of code to it, including the lines a dependency added while you weren't looking, the lines an AI agent wired into the wrong package, and the lines you wrote at 5 PM on a Friday and would have regretted on Monday.

Adopt them in order: capabilities first (one key, instant default-deny, run superj capabilities and tighten), architecture second (expect the first superj topology to teach you something), contracts third (money paths and core types only — don't annotate the world). Each one catches a different class of bug. Together they turn "someone should have caught that" into "the compiler did."

The whole apparatus is one Build.sj key away. Add it, and the next bug in this list is one you never hear about.