A small formal language for specifying systems by their surface (what users experience) and verifying that any chosen substrate (how it's built) refines that surface.
surface {
state { balances : Map[AccountId -> Nat] }
action transfer(from: AccountId, to: AccountId, amount: Nat)
by c: Customer
raises { InsufficientFunds when balances[from] < amount }
then balances[from] -= amount
balances[to] += amount
emit Transferred(from=from, to=to, amount=amount, by=c)
}
substrate SqlMonolith realizes surface {
component Db { ... }
maps { balances = Db.rows }
realizes { surface.transfer(f, t, n) by Db.commit when ... }
}
The user-visible contract and the implementation live side by side. Drift between them becomes mechanically detectable, not a meeting topic.
Read more →Every action declares seven coverage slots — idempotency, auth_channel, retention, rate_limit, observability, availability, freshness. Silence is not a valid design decision; waived: "<reason>" is.
When refinement fails, you get a concrete narrated trace, not a stuck proof. Surface compiles to PlusCal/TLA+ so TLC and Apalache do the heavy lifting.
How it's checked →| Artifact | How |
|---|---|
| Boundary checklist | The seven mandatory action slots fail closed; surfacide check --slots errors on omissions. |
| Static obligations | A consequence-inference pass derives obligations from your declarations (e.g. "you read this cross-substrate aux, so your availability depends on that substrate"). Each must be acknowledged or discharged. |
| Formal model | Compiles to PlusCal/TLA+; TLC/Apalache check invariants, temporal properties, and refinement. |
| Living documentation | A boundary-checklist per action, rendered from the same file the checker uses, so it cannot drift. |
| Security review | actor, attacker, and the auth_channel slot drive integrity-reachability checks: can role X cause effect Y by any chain of allowed actions? |
| Use cases | scenario blocks render to Markdown and are mechanically checked for reachability. |
Rust frontend toolchain — parser, slot pass, obligation pass, docs emit. Single binary, miette-style diagnostics with stable error codes. The compiler talks back so the "what did I forget?" question becomes mechanical.
Read the Surfacide guide →Every error and warning carries a stable code (E_SURFACE_SLOT_MISSING, W_WRITE_CONFLICT, …). Asserted in golden tests. CI-friendly. Searchable.
Run surfacide check . in a terminal next to your editor. The slot pass tells you which of seven mandatory boundaries you've left blank; the obligation pass tells you which cross-cutting consequences need an explicit decision.
Surface is experimental. The language has been shaped by 8 rounds of agent-authored specifications + folded feedback (R1 → R9). See the changelog for per-version history, and the repo for the toolchain and examples.