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

181–190 of 448 posts

Re: AI will make formal verification go mainstream

#181

Post by jcranmer »

rodphil wrote: post #171
simonw wrote: post #2

I'm convinced now that the key to getting useful results out of coding agents (Claude Code, Codex CLI etc) is having good mechanisms in place to help those agents exercise and validate the code they are writing. At the most basic level this means making sure they can run commands to execute the code - easiest with languages like Python, with HTML+JavaScript you need to remind them that Playwright exists and they shou…

> At the most basic level this means making sure they can run commands to execute the code - easiest with languages like Python, with HTML+JavaScript you need to remind them that Playwright exists and they should use it. So I've been exploring the idea of going all-in on this "basic level" of validation. I'm assembling systems out of really small "services" (written in Go) that Claude Code can immediately run and int…

> My intuition is that LLMs will for many use cases lead us away from things like formal verification and even comprehensive test suites. The cost of those activities is justified by the larger cost of fixing things in production; I suspect that we will eventually start using LLMs to drive down the cost of production fixes, to the point where a lot of those upstream investments stop making sense.

There is still a cost to having bugs, even if deploying fixes becomes much cheaper. Especially if your plan is to wait until they actually occur in practice to discover that you have a bug in the first place.

Put differently: would you want the app responsible for your payroll to be developed in this manner? Especially considering that the bug in question would be "oops, you didn't get paid."

Re: AI will make formal verification go mainstream

#182

Post by simonw »

Capricorn2481 wrote: post #173
victorbjorklund wrote: post #67

Earlier quoted context omitted.

AI can do that too? If you have a web app it can use playwright to test functionality and take screenshots to see if it looks right.

But then the AI would theoretically have to write the playwright code. How does it verify it's getting the right page to begin with?

The recent models are pretty great at this. They read the source code for e.g. a Python web application and use that to derive what the URLs should be. Then they fire up a localhost development server and write Playwright scripts to interact with those pages at the predicted URLs.

The vision models (Claude Opus 4.5, Gemini 3 Pro, GPT-5.2) can even take screenshots via Playwright and then "look at them" with their vision capabilities.

It's a lot of fun to watch. You can tell them to run Playwright not in headless mode at which point a Chrome window will pop up on your computer and you can see them interact with the site via it.

Re: AI will make formal verification go mainstream

#185

Post by amw-zero »

bkettle wrote: post #61

I think formal verification shines in areas where implementation is much more complex than the spec, like when you’re writing incomprehensible bit-level optimizations in a cryptography implementation or compiler optimization phases. I’m not sure that most of us, day-to-day, write code (or have AI write code) that would benefit from formal verification, since to me it seems like high-level programming languages are al…

Compare the spec with the application here: https://concerningquality.com/model-based-testing/

I think we've become used to the complexity in typical web applications, but there's a difference between familiar and simple (simple vs. easy, as it were). The behavior of most business software can be very simply expressed using simple data structures (sets, lists, maps) and simple logic.

No matter how much we simply it, via frameworks and libraries or whatever have you, things like serialization, persistence, asynchrony, concurrency, and performance end up complicating the implementation. Comparing this against a simpler spec is quite nice in practice - and a huge benefit is now you can consult a simple in-memory spec vs. worrying about distributed system deployments.

Re: AI will make formal verification go mainstream

#186

Post by amw-zero »

socketcluster wrote: post #154
qingcharles wrote: post #152

Earlier quoted context omitted.

I used to work adjacent to a team who worked from closely-defined specs for web sites, and it used to infuriate the living hell out of me. The specs had all sorts of horrible UI choices and bugs and stuff that just plain wouldn't work when coded. I tried my best to get them to implement the intent of the spec, not the actual spec, but they had been trained in one method only and would not deviate at any cost.

Yeah, IMO, the spec almost always needs refinement. I've worked for some companies where they tried to write specs with precision down to every word; but what happened is; if the spec was too detailed, it usually had to be adjusted later once it started to conflict with reality (efficiency, costs, security/access restrictions, resource limits, AI limitations)... If it wasn't detailed enough, then we had to read betwe…

How do you or the client know that the software is doing what they want?

Re: AI will make formal verification go mainstream

#187

Post by amw-zero »

adverbly wrote: post #167

This smells like a Principia Mathematica take to me... Reducing the problem to "ya just create a specification to formally verify" doesn't move the needle enough to me. When it comes to real-world, pragmatic, boots-on-the-ground engineering and design, we are so far from even knowing the right questions to ask. I just don't buy it that we'd see huge mainstream productivity changes even if we had access to a crystal b…

When you go to write a line of code, how do you decide what to write?

Re: AI will make formal verification go mainstream

#188

Post by ajcp »

infruset wrote: post #134

I was waiting for a post like this to hit the front page of Hacker News any day. Ever since Opus 4.5 and GPT 5.2 came out (mere weeks ago), I've been writing tens of thousands of lines of Lean 4 in a software engineering job and I feel like we are on the eve of a revolution. What used to take me 6 months of work when I was doing my PhD in Coq (now Rocq), now takes from a few hours to a few days. Whole programming lan…

Having known nothing of this field before now I have to say your excitement has me excited!

Re: AI will make formal verification go mainstream

#189

Post by nrhrjrjrjtntbt »

iwontberude wrote: post #46
nrhrjrjrjtntbt wrote: post #6

I love HN because HN comments have talked about this a fair bit already. I think on the recent Erdos problem submission. I like the idea that languages even like Rust and Haskell may be more accessible. Learn them of course but LLM can steer you out of getting stuck.

The idea that LLMs are steering anything correctly with Rust reference management is hilarious to me, but only due to my experiences.

Id definitely use LLMs to troubleshoot but not blindly vibecode.

Re: AI will make formal verification go mainstream

#190

Post by justatdotin »

CyberDildonics wrote: post #153

When people have the choice whether to use AI or use rust because LLMs don't produce workable rust programs they leave rust behind and use something else. The venn diagram of people who want formal verification and think LLM slop is a good idea is two separate circles.

two of my current agent projects use rust: agent generated rust is going very well for me.
Post reply on HN