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

AI will make formal verification go mainstream

martin.kleppmann.com

Post reply on HN
Print view View original

381–390 of 448 posts

Re: AI will make formal verification go mainstream

#381

Post by momojo »

@simonw's successful port of JustHTML from python to javascript proved that an agent iteration + an exhaustive test suite is a powerful combo [0].

I don't know if TLA+ is going to suddenly appear as 'the next language I want to learn' in Stackoverflow's 2026 Developer Survey, but I bet we're going to see a rise in testing frameworks/languages. Anything to make it easier for an agent to spit out tokens or write smaller tests for itself.

Not a perfect piece of evidence, but I'm really interested to see how successful Reflex[1] is in this upcoming space.

[0] https://simonwillison.net/2025/Dec/15/porting-justhtml/ [1] https://github.com/reflex-dev/reflex

Re: AI will make formal verification go mainstream

#382

Post by naasking »

Marazan wrote: post #322
gizmo686 wrote: post #211

Earlier quoted context omitted.

A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…

> For LLMs, there is an added benefit. If you can formally specify what you want, you can make that specification your entire program. Then have an LLM driven compiler produce a provably correct implementation. This is a novel programming paradigm that has never before been possible; although every "declarative" language is an attempt to approximate it. That is not novel and every declarative language precisely embod…

I think most existing declarative languages still require the programmer to specify too many details to get something usable. For instance, Prolog often requires the use of 'cut' to get reasonable performance for some problems.

Re: AI will make formal verification go mainstream

#383

Post by cess11 »

"As the verification process itself becomes automated, the challenge will move to correctly defining the specification"

OK.

"Reading and writing such formal specifications still requires expertise and careful thought."

So the promise here is that bosses in IT organisations will in the future have expertise and prioritise careful thought, or allow their subordinates to have and practice these characteristics.

Would be great news if that'll be the case.

Re: AI will make formal verification go mainstream

#384

Post by nwah1 »

QuadrupleA wrote: post #203

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…

> Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server)

Isn't this what TLA+ was meant to deal with?

Re: AI will make formal verification go mainstream

#385

Post by Verdex »

alexgotoi wrote: post #373

The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…

Yeah, the hyper majority of the history of "getting things done" has been: find some guy who can translate "make the crops grow" into a pile of food.

The people who care about the precise details have always been relegated to a tiny minority, even in our modern technological world.

Re: AI will make formal verification go mainstream

#386

Post by tmtvl »

kazinator wrote: post #324
elbear wrote: post #294

Earlier quoted context omitted.

> No one claims that good type systems prevent buggy software. That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.

If you eliminate the odd integers from consideration, you've eliminated an entire class of integers. yet, the set of remaining integers is of the same size as the original.

There cannot be infinite bugs in a limited program.

Re: AI will make formal verification go mainstream

#387

Post by strbean »

alexgotoi wrote: post #373

The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…

> decide what the software is supposed to do in the first place.

That's where the job security is (and always has been). This has been my answer to "are you afraid for your job because of AI?"

Writing the code is very rarely the hard part. The hard part is getting a spec from the PM, or gathering requirements stakeholders. And then telling them why the spec / their requirements don't make sense or aren't feasible, and figuring out ones that will actually achieve their goals.

Re: AI will make formal verification go mainstream

#388

Post by jandrese »

TimTheTinker wrote: post #377
alexgotoi wrote: post #373

The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…

> it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. Not only that, but it's been well-established that a significant challenge with formally verified software is to create the right spec -- i.e. one that actually satisfies the intended requirements. A formally verified program can still have bugs, because the spec (which requires specialized sk…

The danger of this is people start asking about formally verified specs, and down that road lies madness.

"If you can formally verify the spec the code can be auto-generated from it."

Re: AI will make formal verification go mainstream

#389

Post by Fairburn »

AI is great; it makes my job easier by removing repetitive processes, freeing me up to tackle other "stuff". I like that I can have it form up json/xml scaffolding, etc. All the insanely boring stuff that can often get corrupted by human error.

AI isn't the solution to move humanity forward in any meaningful way. It is just another aspect of our ability to offload labor. Which in and of itself is fine. Until of course it gets weaponized and is used to remove the human aspect from more and more everyday things we take for granted.

It is being used to accelerate the divisions among people. Further separating the human from humanness. I love 'AI' tools, they make my life easier, work-wise. But would I miss it if it wasn't there? No. I did just fine before and would do so after it's flame and innovation slowly peters out.

Re: AI will make formal verification go mainstream

#390

Post by suspended_state »

TimTheTinker wrote: post #377
alexgotoi wrote: post #373

The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…

> it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. Not only that, but it's been well-established that a significant challenge with formally verified software is to create the right spec -- i.e. one that actually satisfies the intended requirements. A formally verified program can still have bugs, because the spec (which requires specialized sk…

> A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.

That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language.

Edit:

I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as "behavioral bug"), but to me it seems to be a misnomer.

I also agree that it's difficult to tell that to a customer when their expectations aren't met.

Post reply on HN