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

When AI writes the software, who verifies it?

leodemoura.github.io

Post reply on HN
Print view View original

141–150 of 309 posts

Re: When AI writes the software, who verifies it?

#141

Post by vicchenai »

The verification problem scales poorly with AI complexity. Current approaches rely on test suites, but AI-generated code tends to optimize for passing existing tests rather than correctness in the general case.

What's interesting is this might be the forcing function that finally brings formal verification into mainstream use. Tools like Lean and Coq have been technically impressive but adoption-starved. If unverified AI code is too risky to deploy in critical systems, organizations may have no choice but to invest in formal specs. AI writes the software, proof assistants verify it.

The irony: AI-generated code may be what makes formal methods economically viable.

Re: When AI writes the software, who verifies it?

#142

Post by cpeterso »

muraiki wrote: post #26

The article says that AWS's Cedar authorization policy engine is written in Lean, but it's actually written in Dafny. Writing Dafny is a lot closer to writing "normal" code rather than the proofs you see in Lean. As a non-mathematician I gave up pretty early in the Lean tutorial, while in a recent prototype I learned enough Dafny to be semi-confident in reviewing Claude's Dafny code in about half a day. The Dafny cod…

Looks like LLMs also find Dafny easier to write than Lean. This study, “A benchmark for vericoding: formally verified program synthesis”, reports:

> We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications … We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs.

https://arxiv.org/html/2509.22908v1

Re: When AI writes the software, who verifies it?

#143

Post by pnathan »

I am experimenting at a very early stage with using Verus in Rust to generate proveably correct Rust. I let the AI bang on the proof and trust the proof assistant to confirm it.

There is another route with Lean where Rust generates the Lean and there is proof done there but I haven't chased that down fully.

I think formal verification is a big win in the LLM era.

Re: When AI writes the software, who verifies it?

#144

Post by muraiki »

dranov wrote: post #125
muraiki wrote: post #26

The article says that AWS's Cedar authorization policy engine is written in Lean, but it's actually written in Dafny. Writing Dafny is a lot closer to writing "normal" code rather than the proofs you see in Lean. As a non-mathematician I gave up pretty early in the Lean tutorial, while in a recent prototype I learned enough Dafny to be semi-confident in reviewing Claude's Dafny code in about half a day. The Dafny cod…

Cedar used to be written in Dafny, but AWS abandoned that implementation and rewrote it in Lean. https://aws.amazon.com/blogs/opensource/lean-into-verified-s...

Oh whoops, thank you for the correction! I didn't realize that.

Re: When AI writes the software, who verifies it?

#146

Post by wyum »

I believe there is a Verification Complexity Barrier

As you add components to a system, the time it takes to verify that the components work together increases superlinearly.

At a certain point, the verification complexity takes off. You literally run out of time to verify everything.

AI coding agents hit this barrier faster than ever, because of how quickly they can generate components (and how poorly they manage complexity).

I think verification is now the problem of agentic software engineering. I think formal methods will help, but I don't see how they will apply to messy situations like end-to-end UI testing or interactions between the system and the real world.

I posted more detailed thoughts on X: https://x.com/i/status/2027771813346820349

Re: When AI writes the software, who verifies it?

#147

Post by Ronsenshi »

A bit unrelated to the article, more of a commentary about how many engineers at this point barely write any code or even do code review.

It seems to me like a huge amount of engineers/developers in comments are turning into Tom Smykowski from The Office. Remember that guy?

His job was to be a liaison between customers and engineers because he had "people skills":

"I deal with the god damn customers so the engineers don't have to. I have people skills; I am good at dealing with people. Can't you understand that? What the hell is wrong with you people?"

Except now, based on comments here it, some engineers are passing instructions from customers to AI because they have "AI skills". While AI is doing coding, helps with spec clarification, reviewing code and writing tests.

That's scary and depressing. This field in a few years will be impossible to recognize.

Re: When AI writes the software, who verifies it?

#148

Post by Herring »

roadbuster wrote: post #139

> The Claude C Compiler illustrates the other side: it optimizes for > passing tests, not for correctness. It hard-codes values to satisfy > the test suite. It will not generalize. This is one of the pain points I am suffering at work: workers ask coding agents to generate some code, and then to generate test coverage for the code. The LLM happily churns out unit tests which are simply reinforcing the existing behavi…

> At no point does anyone stop and ask whether the generated code implements the desired functional behaviour for the system ("business logic").

Obvious question: why not? Let’s say you have competent devs, fair assumption. Maybe it’s because they don’t have enough time for solid QA? Lots of places are feature factories. In my personal projects I have more lines of code doing testing than implementation.

Re: When AI writes the software, who verifies it?

#149

Post by bandrami »

Hammershaft wrote: post #129
candiddevmike wrote: post #127

Earlier quoted context omitted.

> and it wasn't long ago before LLMs couldn't do math They still can't do math.

Pro models won gold at the international math olympiads?

They have trouble adding two numbers accurately though

Re: When AI writes the software, who verifies it?

#150

Post by jmathai »

GoatInGrey wrote: post #82
fmbb wrote: post #78

Earlier quoted context omitted.

There are still no successful useful vibe codes apps. Kernels are pretty far away I think.

To be fair, Claude Code is vibe-coded. It's a terrible piece of software from an engineering (and often usability) standpoint, and the problems run deeper than just the choice of JavaScript. But it is good enough for people to get what they want out of it.

> But it is good enough for people to get what they want out of it.

This is the ONLY point of software unless you’re doing it for fun.

Post reply on HN