Formal Verification Gates for AI Coding Loops

When AI agents generate thousands of lines of code, it's difficult to actually confirm whether security invariants were upheld. Even if you emphasize in the prompt that "permission validation is very important," the model can forget or skip it, and tests are empirical—they only check the cases that were written.

Shen-Backpressure solves this problem with structural constraints. The core idea is to use a structural gate (compiler, type checker, proof checker) instead of a behavioral gate (instructing the model via prompt to "not do X").

How it works:

• Write invariants as formal specifications in the Shen language (e.g., "a user can access a resource only if they are authenticated, a tenant member, and the resource belongs to that tenant")
• The shengen code generator converts this into guard types in the target language (Go, TypeScript, etc.)
• The generated types are sealed so they cannot be created without a correct proof (in Go's case, via unexported fields + smart constructors)
• If an AI agent skips the proof chain, the build fails

A verification loop composed of 5 gates:

1. shengen: Checks synchronization between the Shen spec and generated code
2. test: Runtime invariant and regression tests
3. build: Detects type mismatches and incorrect use of proof chains
4. shen tc+: Checks internal consistency of the Shen spec
5. tcb audit: Detects manual edits to generated guard code

Gate failures are fed back into the next prompt as specific context, forming a backpressure in the style of the Ralph loop. It can be integrated with Claude Code, Cursor, Codex, and others, and installed into a project with sb init.

In a multi-tenant API demo, instead of repeating permission validation logic as if statements in each handler, it was concentrated at the point where the TenantAccess type is created. If an agent tries to bypass this, a compile error occurs.

The limitations are also clear. There is a cost to writing specifications, the generated guard code cannot be manually edited, and it depends on the strength of encapsulation in the target language. In Go's case, bypassing via reflection or package-internal code is theoretically possible. However, the author argues that even just making accidental bypasses structurally difficult provides high leverage in an environment of AI-generated code.