[pyrex41]

The distinction worth keeping clean is between the spec (here, written as proofs in Shen) being formally rigorous and the entire codebase being formally verified. Shen-Backpressure does the first: the spec is a sequent-calculus statement of invariants, and shengen lowers it into guard types the target compiler refuses to violate, so within the target language's type discipline you cannot construct a tenant-access (or any other witness) without discharging its premises.

It does not do the second (formally verify the entire codebase). Outside the guard types your Go or TypeScript is just code. It can panic, race, have bugs in unrelated logic, use reflection to forge values inside the guard package, get a wrong answer from the SQL query that fed the predicate, and so on. The proof ends at the projection boundary.

Why not go further? Not really "too complex to implement," in theory; it has been done before. But verifying the whole program is much higher engineering cost, and the trades-offs to do it make sense in a much narrower set of cases than what I'm trying to target: teams shipping production code with AI in the loop, in the language they already ship.

The pragmatic choice is to spend the verification budget on the small set of invariants that genuinely matter and leave the rest as ordinary code with ordinary review and tests. That is why the claim is phrased as "practically impossible to accidentally bypass, not categorically impossible to bypass." Over-claiming "verified" when the host language is unverified would be misleading.

[Mikhail_K]

Thanks. Why the shen language was selected for writing specifications?

[pyrex41]

Learning about Shen is what inspired the project for me. Combination of sequent calculus and prolog in a highly portable lightweight kernel that is easy to port to many runtimes (https://shen-language.github.io) gives a ton of expressive power. If you only want compile-time checks, plenty of other notations work. What actually interests me is the possibility of a single spec whose invariants produce enforcement that crosses compile time (guard types + shen tc+) and runtime (generated checks in constructors, plus the spec itself as a test oracle via shen-derive), with no translation layer required between them.