sb

Shen-Backpressure

Formal verification gates for AI coding loops, in the language you're already using.

The Problem

AI coding loops use tests as the only gate. Tests are empirical: they check the cases you remembered to write. Specs are deductive: they hold for every case the type system can construct. An LLM that produces code which slips past your tests but contradicts an invariant has produced a regression that won't surface until production.

Shen-Backpressure adds spec-level gates to the loop. The agent must pass the structural check (your invariants compile) and the behavioral check (your pure functions match a spec on sampled inputs) on top of the regular tests and build. When a gate fails, the failure feeds back into the next prompt as backpressure.

What Shen-Backpressure Does

You write a Shen sequent-calculus spec describing your domain's invariants and pure functions. The spec lives in your repo as specs/core.shen and is the human-edited source of truth.

shengen lowers the spec into opaque guard types in your target language. Today: Go and TypeScript are production-wired through sb gen; Python and Rust exist as reference emitters. The guard types have unexported fields and validated constructors, so the language compiler enforces every invariant the spec declares. shen-derive turns (define …) spec blocks into table-driven tests that pin a hand-written implementation against the spec on sampled inputs.

Production ships your normal target-language binary. Shen runs at build time, not at runtime — but the two guarantees are different in kind. Structural guarantees (shen-guard) are compile-time: the target-language compiler rejects any Amount that wasn't built through NewAmount. Behavioral evidence (shen-derive) is sampled: a deterministic boundary pool plus optional seeded random draws asserts pointwise equality between the spec and the impl. The former is a proof-for-all-inputs; the latter is high-confidence evidence on a designed sample.

The Five Gates

Every iteration of the Ralph loop must pass all five gates (plus a sixth when shen-derive is configured):

Gate	Command	What it catches
1. shengen	sb gen	Regenerates guard types from spec. Catches stale types.
2. test	go test ./... (or npm test)	Tests against regenerated types. Catches runtime invariant violations.
3. build	go build ./... (or npx tsc --noEmit)	Compiles against regenerated types. Catches type signature mismatches.
4. shen tc+	bin/shen-check.sh	Verifies spec internal consistency. Catches contradictory rules.
5. tcb audit	bin/shenguard-audit.sh	Re-runs shengen, diffs output, rejects unexpected files in shenguard/.
6. shen-derive	sb derive	Regenerates committed spec-equivalence tests, fails on drift, then runs them. Active when [[derive.specs]] is configured.

Gate topology is declared in sb.toml. The legacy fixed five-gate shape still works; the new [[gates]] array of tables lets you declare a custom gate list with optional parallel groups.

Discharge Reports — Audit-Grade Verification Artifacts

Every successful gate run also writes .sb/discharge_report.json, a structured artifact that distinguishes how each premise of each Shen rule was discharged: statically by the guard types, by runtime sampling against the Shen oracle, or unproven. Failed premises ship with concrete counter-examples — case ID, spec output, impl output, and a ready-to-paste go test -run … reproduction command.

The artifact is dual-purpose:

• Agent-loop backpressure. sb context injects a five-second Markdown summary into the harness prompt. Failed cases steer the next iteration without scraping log output.
• Audit-grade verification artifact. sb audit-report renders a long-form Markdown document a security reviewer or compliance auditor can read end-to-end without prior knowledge of Shen-Backpressure: spec hash, git commit, tool versions, per-rule premise tables, history, and a "How to read this report" appendix.

The schema is locked at schema_version: 1 (design memo) and time-stamped copies accumulate under .sb/history/ so claims like "this invariant has been verified at every commit since X" have evidence on disk, not memory.

What this does not mean: not signed, not third-party verified, not SOC-2 certified. The artifact is the foundation that audit and compliance workflows can build on — not certification itself. The schema reserves room for signature fields; v0 always emits signature: null.

Quick Start

# In your project (sb binary on $PATH)
sb init        # scaffold specs/core.shen, sb.toml, prompts/, plans/
               # and install /sb:* commands into .claude/
sb loop        # run the Ralph loop