Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formal Verification Gates for AI Coding Loops

reubenbrooks.dev

Post reply on HN
Print view View original

31–40 of 40 posts

Re: Formal Verification Gates for AI Coding Loops

#31

Post by ianhorn »

I've been experimenting with this a lot lately in Lean because it's equally capable as a theorem prover and as a programming language. It's resolving a lot of the frustration I feel with LLM coding.

You write a type signature for a function that amounts to "take a Foo x and return a Bar y with a proof of does_what_i_wanted(x,y)." Voila, no more agents doing something else because it won't compile if they don't do what I wanted.

It's great to build faster without the frustration of having no confidence in what I build. But it sure makes the gap between toys in Lean and using this in a Real Project in some other language that much more frustrating.

Re: Formal Verification Gates for AI Coding Loops

#32

Post by se4u »

pyrex41 wrote: post #2

Author here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-Backpressure. Builds a lot on Geoff Huntley's backpressure idea -- none of this is rocket science, just an effort to apply sound programming principles in a world of LLM coding agents.

Hi, thanks for the writeup, I wonder for the auth problem what you think about rego and OPA type solutions and their place in world in comparison to generated guards?

Re: Formal Verification Gates for AI Coding Loops

#33

Post by ianhorn »

solomonb wrote: post #14

This is really cool, but why wouldn't you just use a more richly typed target language and skip this process? You could use Liquid Haskell (for refinement types) or Lean (for full dependent types) and be able to put these invariants directly in your program rather then in a sidecar.

Not the author, but I've been doing this kind of thing with Lean. I'm still trying to figure out how to make this workflow play nicely with other systems. I have a bunch of rust code that I want these kinds of guarantees on, and that code has third party dependencies that would be terrible to give up. It's totally unclear right now how to get the best of both worlds.

Re: Formal Verification Gates for AI Coding Loops

#34

Post by henrymerrilees »

max_unbearable wrote: post #11

This matches my experience running coding agents daily: the agent is reliable at producing the shape of a thing and unreliable at holding an invariant across a long loop. Moving the rule into a type the compiler won't violate works because it relocates the check to the one place the loop can't quietly skip. But singron's JWT point is the real limit. Backpressure doesn't remove the judgment, it moves it. The type stil…

Why even post this?

Re: Formal Verification Gates for AI Coding Loops

#35

Post by Twirrim »

alexpotato wrote: post #12

I work in DevOps at a firm that has been very enthusiastic about using LLMs (in the good sense). The phases were basically: - try out having the LLM do "a lot" - now even more - now run multiple agents - back to single agents but have the agents build tools - tools that are deterministic AND usable by both the humans (EDIT: and the LLMs) The reasons: 1. Deterministic tools (for both deployments and testing) get you a…

I've a bunch of technical, but non-engineering types around me, and a few of us engineers keep banging the gong on the fact that they can't trust the output of an LLM. That the best way to leverage AI is to get it to write the code in whatever language they prefer, so they get a simple and repeatable tool out the other side. In many regards it's a liberating tool when used like that. I've got TPMs that are really able to use it as a force multiplier for themselves, building small tools that help them, without having to tie up engineers to produce it.

In numerous cases, though, there are folks asking it to go interrogate some stuff they've set up MCPs for, and produce reports from it. If you do that it will give you a different answer every time, even from exactly the same input (because that's how LLMs work) and you just can't guarantee that any of them are accurate. It's a probabilistic layer, and the reports you need to generate need to be deterministic.

The problem is we're so accustomed to the deterministic nature of the large majority of the software we work with. The output is plausible, too, which only exasperates the problem. Folks just assume it's correct.

Re: Formal Verification Gates for AI Coding Loops

#37

Post by pyrex41 »

se4u wrote: post #32
pyrex41 wrote: post #2

Author here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-Backpressure. Builds a lot on Geoff Huntley's backpressure idea -- none of this is rocket science, just an effort to apply sound programming principles in a world of LLM coding agents.

Hi, thanks for the writeup, I wonder for the auth problem what you think about rego and OPA type solutions and their place in world in comparison to generated guards?

Definitely connected; OPA is itself a structural gate, but at runtime. The post focused on compile-time gates, but there's no reason a structural gate can't run at runtime — which means they compose rather than compete.

I didn't get into this in the post, but Shen is extremely portable and has been ported to a lot of different target runtimes (Go, C, Lisp, JS, many others — https://shen-language.github.io/#downloads). But, OPA offers extremely fast runtime execution in a way that would be more difficult to get to in Shen. What the compile-time guard adds is that it can make the runtime invocation non-skippable — so you could have a compile-time assertion that the code calls the runtime assertion, with OPA sitting behind the constructor. The catch is that if you still want all your invariants in Shen but use OPA for the runtime layer, that's another translation layer to keep in sync (Shen → Rego alongside Shen → guards). The alternative is to lean on Shen's portability: you could run the same spec at runtime with no translation layer at all, trading OPA's speed for that simplicity. Either way they're similar concepts run at different times. Integrating both into one high-level spec is mostly a question of which of those tradeoffs you want.

Re: Formal Verification Gates for AI Coding Loops

#38

Post by Mikhail_K »

pyrex41 wrote: post #8
Mikhail_K wrote: post #5

Earlier quoted context omitted.

Thank you, interesting work. Please, clarify what is possibly a naive question - your README states that the constraints imposed by your tool are weaker than the formal verification guarantees. Why not implement the backpressure as the full formal verification barrier? Too complex to implement?

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…

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

Re: Formal Verification Gates for AI Coding Loops

#39

Post by fractallyte »

henrymerrilees wrote: post #34
max_unbearable wrote: post #11

This matches my experience running coding agents daily: the agent is reliable at producing the shape of a thing and unreliable at holding an invariant across a long loop. Moving the rule into a type the compiler won't violate works because it relocates the check to the one place the loop can't quietly skip. But singron's JWT point is the real limit. Backpressure doesn't remove the judgment, it moves it. The type stil…

Why even post this?

Because it's exactly relevant, and adds more to the discussion.

Re: Formal Verification Gates for AI Coding Loops

#40

Post by pyrex41 »

Mikhail_K wrote: post #38
pyrex41 wrote: post #8

Earlier quoted context omitted.

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…

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

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.
Post reply on HN