Shen-Backpressure

New here? Start with the series introduction — Structural Backpressure Beats Smarter Agents — for the full thesis, a working multi-tenant authorization demo, and how to wire the gated loop into your own project.

Shen-Backpressure is the backend and orchestration side of the same broader idea: do not ask an agent to remember the invariant if you can move the invariant into a structure the agent cannot bypass.

In practice that means a Shen spec, generated guard types, and a gate pipeline that keeps feeding hard feedback back into the coding loop. The model does not have to understand sequent calculus in any deep sense. It has to make the code compile, pass tests, and stay aligned with the generated types. The proof machinery lives underneath that feedback surface.

Core Pieces

• sb, a manifest-driven engine for running project-specific gate topologies.
• shengen, which turns Shen datatype rules into opaque guard types in Go or TypeScript.
• shen-derive, which uses pure Shen functions as spec oracles for generated equivalence tests.
• Example systems that show the pattern in payments, authorization, state machines, and polyglot tooling.

Why I Keep Coming Back To It

Most AI coding workflows still lean hardest on tests. Tests are useful, but they are empirical and sparse. Shen-Backpressure adds higher-density feedback: type errors, generator drift, spec inconsistencies, and audit failures. That is the “backpressure” in the name. Instead of waiting for bad states to leak outward, the loop refuses them early and noisily.

Witness is the most visually striking descendant of this idea, because it applies the same structural logic to UI overflow. Shen-Backpressure is the more general pattern. Write the invariant once, project it into multiple enforcement surfaces, and let the loop learn from the failure boundary instead of from vibes.