Shen-Backpressure encodes access-control invariants as Shen sequent-calculus types, generates guard types via shengen, and pipes compiler refusals back into AI coding loops as concrete backpressure.
Key Takeaways
Behavioral gates (prompt rules, CLAUDE.md, checklists) fail at scale; structural gates (compiler, type checker, proof checker) produce deterministic refusals the loop can push against.
The tool lowers Shen specs into unexported Go or TypeScript guard types with smart constructors; code that skips the proof chain fails to build before a binary exists.
Multi-tenant auth is the demo: a full chain jwt-token > authenticated-user > tenant-access > resource-access must be traversed; skipping any step causes a compile error, not a runtime bug.
Five default gates run per iteration: shengen (spec drift), go test (regressions), go build (type mismatches), shen tc (spec consistency), and shenguard-audit (hand edits to generated guards).
Limits are explicit: Go reflection and zero values are escape hatches; a bad SQL query can hand the constructor a wrong boolean; the claim is bypass-by-accident is hard, not bypass-at-all is impossible.
