Formal Verification Gates for AI Coding Loops

I mean yes, that's a risk, and you are correct. In practice, is your spec about the shape of the app you want to build really going to be that complicated?

But I mentioned its Turing completeness as a lazy shorthand to illustrate that it is far more flexible and expressive than what people think of as a "type system". https://shenlanguage.org/OSM/Recursive.html

For a single-language Rust project with a handful of invariants, not much. Rust's newtypes + private fields + Result-returning constructors are exactly the right primitives, and they're strictly stronger than Go's (no reflection escape hatch, no zero values to forge, exhaustive matching).

Where shengen might be more interesting:

1. Multi-language emit. If your invariants live in a Rust service AND a TypeScript frontend (or another backend), one Shen spec drives both and the build catches drift. Hand-rolled means writing the same smart constructor twice in two languages with no mechanism to keep them in lockstep.

2. Spec as the audit surface. The Shen rule for `tenant-access` is going to be much more expressive / concise than the rust implementation. The `tcb-audit` gate fails the build if generated code is hand-edited away from the spec, so reviewers read the spec and the build polices the implementation against it. With hand-rolled Rust you're reviewing the impl directly — which isn't strictly bad, but it does potentially insert the human back into the loop between LLM iterations.

3. AI in the loop. If you're hand-writing the constructors carefully yourself, the argument for shengen is fairly weak. If an LLM is writing them, "declarative spec + codegen" is, in my experience, a stronger prompt than "describe the constructor in precise English." That's the frame the post is really written for; the Rust newtype point is well-taken outside it.

I'm not saying everyone writing software (w/ LLMs or not) needs shengen / shen-backpressure. The underlying principles it's trying to help you use aren't new at all. But, if you want to get more out of LLMs (esp. multi-turn loops), you probably need something that is deterministic and structured to provide that backpressure context you want to the LLM as it iterates.

What I've learned so far is that the tooling mentioned in this article can have dual purpose. Sure you can use it to gate the agent but you can also use them as tools for the agents to understand what they are working with at a more abstract level and with less tokens required.

In a way, you push some of the reasoning into deterministic tooling which is great both for reliability and performance.

At least on what I've been working on where I ended up creating type systems over SQL to solve some of the annoying issues I was having with agents reasoning over complex data infrastructure.

My naive thoughts on Formal Verification (FV) and LLM:

We could leverage existing FV tools for a given programming language by using an LLM to generate a translator that maps the language to the FV tool's input format. This would essentially require a finite number of "abstract interpretation" functions—one for each language construct. While the total number of constructs might be large (e.g., around 500), each function would be independent. A function would only need to reason about the abstract semantics of a single construct, assuming the others adhere to their respective semantics. We could then distribute these LLM-generated functions among a group of experts (e.g., 100 reviewers). Thanks to the modularity of the functions, reviewers could evaluate their assigned subset in parallel without bottlenecks. The end result would be a working FV tool for the target language.

I've had similar thoughts lately while using agents for coding. It seems like if I give the agents external tools and sources of truth they perform really well. In my case it was a lot of standards, extensive use of Rust language features (e.g. traits), formal methods tools, large-scale architecture and specification documents (accessed via a special tool I also wrote), and using the beads_rust tool for tracking session state and giving the agent a list of issues to work. I hadn't thought of this as 'backpressure' but I really like that framing. It gives the agents guardrails and context and external validity that it can't make up.