The structural-safety wedge: capabilities + contracts

The previous post took fastC up to the stdlib MVP — a language that compiles non-trivial programs but has not yet earned its name. This post is where the wedge lands. Two stages, stage 1.4 (capabilities) and stage 1.5 (contracts), plus stage 2.1 (the SMT discharger that makes contracts cheap), are the work that distinguishes fastC from “C with a nice type system.” Neither of these claims can be retrofitted onto Rust without breaking the ecosystem. That is the structural part.

We will be careful about what we are claiming. Rust still wins on the static memory-safety guarantee that does not depend on runtime. Capabilities and contracts are different properties, and they compose with Rust’s properties rather than replacing them. If you read this post hearing “fastC is safer than Rust,” you have heard the wrong thing. The right thing is “fastC adds two structural properties Rust does not have, at the cost of the property fastC does not have.”

Stage 1.4 — the eight capability types

The capability types are sealed structs in mod caps:

• CapFsRead — filesystem reads
• CapFsWrite — filesystem writes
• CapNetConnect — outbound network connections
• CapNetListen — inbound network listeners
• CapProcSpawn — spawning child processes
• CapTimeRead — reading the wall clock
• CapRand — entropy source for random_bytes
• CapEnvRead — reading environment variables

The set is finite. There is no CapAnyIO; there is no CapDoWhatever. If we need a new I/O surface, it gets a new cap. The names are visible in caps::init(), in the caps.json artifact emitted per build, and in every function signature that needs one.

The minting rule is the load-bearing piece: every cap is mintable exactly once, in main, via a single call to caps::init() -> Caps. The Caps struct holds the eight sealed fields. From there, references flow downward through function arguments.

A function that wants to read the filesystem has a signature like this:

fn read_file(c: ref(CapFsRead), path: raw(u8)) -> opt(Str) {
    return fs::read(c, path);
}

The caller has to have a ref(CapFsRead) to pass. That caller’s caller has to have one. All the way up the chain, the cap originates in main. A function that does not declare a cap in its signature structurally cannot reach for the resource — the compiler refuses the call to fs::read from any body whose function does not have a ref(CapFsRead) in scope.

The compile error, when a cap is dropped, is concrete:

error[E0410]: cannot call `fs::read` from a function that does not carry `CapFsRead`
  --> src/parse_args.fc:14:5
   |
14 |     let bytes: opt(Str) = fs::read(path);
   |                           ^^^^^^^^ requires `ref(CapFsRead)`
   |
help: add the capability to the function signature:
   |
12 | fn parse_args(c: ref(CapFsRead), args: Vec[Str]) -> i32 {
   |               ++++++++++++++++++

The fix-it adds the cap to the signature. The reviewer reading the diff sees the cap appear in the signature. The I/O surface of the function is now visible from outside.

The other half of the enforcement is the fabrication check. The cap structs are sealed: their fields are private to mod caps, and the constructor is pub only inside mod caps. A fabrication-check pass runs in stage 1.4 that refuses any code outside mod caps from constructing a sealed cap struct. This closes the obvious workaround (“just write CapFsRead {} yourself”). The pass is conservative — it flags any struct literal expression whose path resolves to a sealed type — and the compile error points at the offending literal.

The caps.json artifact is the audit surface. Every build emits a JSON file listing which caps each public function in the crate transitively requires:

{
  "version": 1,
  "module": "my_app",
  "functions": {
    "my_app::parse_config": {"caps": ["CapFsRead"]},
    "my_app::send_metrics": {"caps": ["CapNetConnect", "CapTimeRead"]},
    "my_app::pure_helper":  {"caps": []}
  }
}

This is what fastc-mcp serves to Claude Code, Cursor, and Codex over MCP. The agent that wants to know whether a function does I/O does not text-parse the source — it queries the caps.json resource and gets the typed answer.

Stage 1.5 — contracts as first-class annotations

@requires and @ensures are not comments. They sit above the function signature and the compiler enforces them.

@requires(divisor != 0)
@requires(divisor > 0)
@ensures(result * divisor + (value % divisor) == value)
fn safe_div(value: i32, divisor: i32) -> i32 {
    return (value / divisor);
}

@requires clauses are checked at function entry; the first that fails wins. @ensures clauses are checked at every return site, where the identifier result is bound to the value about to be returned. The v1 lowering is straightforward: @requires becomes a if (!cond) fc_trap() at the function entry; @ensures becomes the same check immediately before each return.

The runtime cost on the hot path is real but small. A contract that lowers to two integer comparisons adds a few nanoseconds per call. The cost we worry about is the expressive cost — a contract that does substantial computation inside the predicate (a quantifier, a recursive helper) can be the dominant cost of the function. We have linting that flags this; the canonical workaround is to factor the predicate into a helper function that is @purity(pure) and call it from both @requires and the body.

The result keyword in @ensures is the part agents take a beat to learn. It is not a variable in the body; it is the value at the return site. An LLM that first writes @ensures(result == value / divisor) and then writes return value / divisor; produces a contract that proves trivially. That is fine — it is the documentation case. The contract that actually catches a bug is the one that constrains something the body does not obviously compute.

Stage 2.1 — the three-tier discharge pipeline

Runtime traps are correct but expensive. Every @requires that lowers to a runtime check is a check the CPU runs at every call. Stage 2.1 was the work to move as many of those checks as possible to compile time.

The pipeline has three tiers, applied in order:

Tier 1: syntactic discharge. Pattern-match the obligation against a small set of tautologies. If cond is (x > 0) || (x == 0) || (x < 0) the discharger recognizes it as a tautology over i32 and discharges without invoking the SMT solver. If cond is x == x, same. If cond is provably true from a straight-line return — e.g., @ensures(result == 42) over a body return 42; — the discharger constructs the equality, recognizes it, and discharges. This tier is fast (microseconds per obligation), always on, and requires no external dependencies.

Tier 2: Z3. Anything tier 1 cannot prove and that fits the SMT fragment (linear integer arithmetic, bitvectors, equality, boolean structure) is encoded as an SMT-LIB query and shipped to Z3 with a per-obligation budget of 500 ms. The encoding is body-aware for straight-line returns: the discharger walks the body’s straight-line path, builds a symbolic state, and asserts the postcondition against that state. Branches are handled by case-splitting; loops are not — a function with a loop in its straight-line path falls through to tier 3 unless the loop has a recognized shape (a counted loop with a constant bound, primarily).

Tier 3: runtime fallback. Anything tiers 1 and 2 cannot prove lowers to the v1 runtime trap. The discharger does not block the build; it records the obligation as runtime-discharged in discharge.json.

The discharge artifact looks like this:

{
  "version": 1,
  "obligations": [
    {
      "function": "my_app::safe_div",
      "kind": "requires",
      "expr": "divisor != 0",
      "tier": "z3",
      "result": "proved",
      "duration_ms": 4
    },
    {
      "function": "my_app::abs",
      "kind": "ensures",
      "expr": "result >= 0",
      "tier": "syntactic",
      "result": "proved",
      "duration_ms": 0
    },
    {
      "function": "my_app::parse_int",
      "kind": "ensures",
      "expr": "result.is_some() || input_was_empty",
      "tier": "runtime",
      "result": "deferred",
      "duration_ms": 0
    }
  ]
}

The reviewer reading discharge.json sees which contracts are static and which are runtime. The agent reading discharge.json (via MCP) sees the same. Runtime discharge is a fallback, not a failure — but a function whose contracts all discharged at runtime is a function whose contracts are documentation, not enforcement.

The on-disk per-formula cache is the speedup that makes this practical. Each obligation is keyed by a hash of its SMT-LIB encoding; the result is cached in .fastc/discharge/<hash>.json. A clean rerun against an unchanged crate hits the cache for every obligation. The measured speedup is ~18x on the eleven curated fastc-core packages; the unchanged-obligation rate in a working session tends to be very high.

A worked tautology

The toy example we use in the docs:

@ensures((x > 0) || (x == 0) || (x < 0))
fn classify(x: i32) -> i32 {
    if (x > 0) { return 1; }
    if (x == 0) { return 0; }
    return -1;
}

Without the discharger, this is three runtime checks (one per return site). With the discharger, tier 1 recognizes the predicate as a tautology over i32 (the trichotomy axiom is built in), proves all three obligations in microseconds total, and the runtime check disappears from the C output. The reviewer reading the generated C sees three plain returns, no fc_trap call.

Honest caveats

Contracts only help if you write them. The agent that does not write @requires gets no contract enforcement. The reviewer who does not insist on contracts in the PR diff gets no contract enforcement. The structural piece is that the language has the surface; the policy piece is that the team uses it.

Z3 is not magic. Many useful properties are outside the SMT fragment fastC encodes — anything quantified over an unbounded loop, anything involving recursive data structures, anything involving real arithmetic. Those fall to tier 3 (runtime). The discharger is honest about this in discharge.json.

Capabilities catch the call, not the misuse inside the body. A function with CapProcSpawn still has to escape its arguments correctly when it shells out. The compiler has not solved shell escaping. What the compiler has done is bound the attack surface to “the small set of functions that explicitly carry CapProcSpawn” — the reviewer reads those carefully, not every function in the codebase.

Rust’s borrow checker remains the gold standard for static memory-safety. fastC’s contracts plus runtime trap layer get strong defaults for typical agent-generated code, but the threat model where memory safety must hold without any runtime check is one where Rust still wins. The honest answer is that fastC and Rust make different trades, and the working environment we built fastC for is the one where the capability + contract trade pays.

The next post is supply-chain and cross-compile — the work that makes the structural-safety story extend out to “you can trust your dependency tree” and “you can ship to eight targets from one source tree.”