Claim: Capabilities

This is one of the four claims March 1.0 makes and treats any break of as a bug. Each claim page says the same four things: the guarantee, what it assumes, what it does not claim, and the CI check that defends it. The other three are deploys, performance and refinement types.

The full reasoning, layer by layer, is on the Capability Threat Model page.

The guarantee

A March program can only reach the capabilities main is granted: a program that could reach anything more does not compile. Every module, including every dependency, declares in needs what it touches, and the compiler checks those declarations against the code it actually emits, so a module that uses something it did not declare does not compile either. A Cap(X) value can’t be forged or widened, only received and narrowed. If you also compile with --cap-sandbox, or launch with forge cap run, the operating system enforces the grant on the running process, for the capabilities it can tell apart, and the program refuses to start if the sandbox can’t be put in place.

Assumptions

  • The compiler, runtime and standard library are correct. The checks are a whole-program analysis, not a machine-checked proof.
  • Every language form is visited by the capability walks (not yet tested mechanically; see Gate).
  • You build with the default checks (--no-cap-strict turns part of them off).
  • The program reaches no C code (extern), or you trust the C code it reaches. A program that reaches C can only be built with the full grant, Cap(IO).
  • For the run-time part: you opted into --cap-sandbox or forge cap run, on a tier-1 platform (darwin-arm64, linux-x86_64, linux-aarch64). The sandbox is opt-in in 1.0 (decided 2026-10-30).

Not claimed

  • Per-function bounds. Functions inside a module share the module’s needs. A declared per-function bound is planned, not built.
  • What code does with a capability it holds, or what it prints to the console.
  • Hot-patched code. A hot deploy is checked against the patch’s own signed list of capabilities and an optional node policy, not against what the patch’s code does.
  • Protection from whoever builds the binary. They choose whether --cap-sandbox is in it. For code you don’t trust, use forge cap run --allow-only.
  • Capabilities the OS can’t enforce. IO.FileRead under --cap-sandbox, and IO.Clock, IO.Spawn, IO.Console, IO.Random, IO.Foreign everywhere, are advisory.

Gate

Runs in CI today:

  • The capability tests in the run_compiler suite (test/test_cap_*.ml: the upper limit, unforgeability, scopes, symbols, the sandbox profile, and --cap-sandbox running real binaries), in the test (ubuntu, compiler) and test (macos-15, all) jobs.
  • The capability programs in the static-semantics reject corpus (specs/lang/types/reject/), in the conformance job.

Planned, not built:

  • A walk-completeness test proving every syntax-tree and IR constructor is visited by every capability walk.
  • A must-reject corpus: one program per past capability bypass.

Until both exist, this claim is defended by unit tests and review, not by a gate that would catch the next missed language form.