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

261–270 of 448 posts

Re: AI will make formal verification go mainstream

#261

Post by planckscnst »

formerly_proven wrote: post #10
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…

Not so sure about formal verification though. ime with Rust LLM agents tend to struggle with semi-complex ownership or trait issues and will typically reach for unnecessary/dangerous escape hatches ("unsafe impl Send for ..." instead of using the correct locks, for example) fairly quickly. Or just conclude the task is impossible. > automatic code formatters I haven't tried this because I assumed it'll destroy agent p…

I've directly faced this problem with automatic code formatters, but it was back around Claude 3.5 and 3.7. It would consistently write nonconforming code - regardless of having context demanding proper formatting. This caused both extra turns/invocations with the LLM and would cause context issues - both filling the context with multiple variants of the file and also having a confounding/polluting/poisoning effect due to having these multiple variations.

I haven't had this problem in a while, but I expect current LLMs would probably handle those formatting instructions more closely than the 3.5 era.

Re: AI will make formal verification go mainstream

#263

Post by akrauss »

thomasfromcdnjs wrote: post #135
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…

shameless plug: I'm working on an open source project https://blocksai.dev/ to attempt to solve this. (and just added a note for me to add formal verification) Elevator pitch: "Blocks is a semantic linter for human-AI collaboration. Define your domain in YAML, let anyone (humans or AI) write code freely, then validate for drift. Update the code or update the spec, up to human or agent." (you can add traditional linte…

Quick feedback: both the „learn more“ link at the very top and the „Explore all examples“ link lead to 404

Re: AI will make formal verification go mainstream

#264

Post by metalrain »

I think we will use more tools to check the programs in the future.

However I don't still believe in vibecoding full programs. There are too many layers in software systems, even when the program core is fully verified, the programmer must know about the other layers.

You are Android app developer, you need to know what phones people commonly use, what kind of performance they have, how the apps are deployed through Google App Store, how to manage wide variety of app versions, how to manage issues when storage is low, network is offline, battery is low and CPU is in lower power state.

Re: AI will make formal verification go mainstream

#265

Post by jeffreygoesto »

Almondsetat wrote: post #257
est wrote: post #227

Earlier quoted context omitted.

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good

That is one problem of many solved, isn't that good?

That the spec solves the problem is called validation in my domain and treated explicitly with different methods.

We use formal validation to check for invariants, but also "it must return a value xor an error, but never just hang".

Re: AI will make formal verification go mainstream

#266

Post by akrauss »

planckscnst wrote: post #251
WhyOhWhyQ wrote: post #38

Earlier quoted context omitted.

I've tried getting claude to set up testing frameworks, but what ends up happening is it either creates canned tests, or it forgets about tests, or it outright lies about making tests. It's definitely helpful, but feels very far from a robust thing to rely on. If you're reviewing everything the AI does then it will probably work though.

LLMs are very good at looking at a change set and finding untested paths. As a standard part of my workflow, I always pass the LLM's work through a "reviewer", which is a fresh LLM session with instructions to review the uncommitted changes. I include instructions for reviewing test coverage. I've also found that LLMs typically just partially implement a given task/story/spec/whatever. The reviewer stage will also no…

What tooling are you using for the orchestration?

Re: AI will make formal verification go mainstream

#267

Post by planckscnst »

zahlman wrote: post #54
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…

One objection: all the "don't use --yolo" training in the world is useless if a sufficiently context-poisoned LLM starts putting malware in the codebase and getting to run it under the guise of "unit tests".

For now, this is mitigated by only including trusted content in the context; for instance, absolutely do not allow it to access general web content.

I suspect that as it becomes more economical to play with training your own models, people will get better at including obscured malicious content in data that will be used during training, which could cause the LLM to intrinsically carry a trigger/path that would cause malicious content to be output by the LLM under certain conditions.

And of course we have to worry about malicious content being added to sources that we trust, but that already exists - we as an industry typically pull in public repositories without a complete review of what we're pulling. We outsource the verification to the owners of the repository. Just as we currently have cases of malicious code sneaking into common libraries, we'll have malicious content targeted at LLMs

Re: AI will make formal verification go mainstream

#269

Post by 71bw »

metalrain wrote: post #264

I think we will use more tools to check the programs in the future. However I don't still believe in vibecoding full programs. There are too many layers in software systems, even when the program core is fully verified, the programmer must know about the other layers. You are Android app developer, you need to know what phones people commonly use, what kind of performance they have, how the apps are deployed through…

LLMs can handle a lot of these issues already, without having the user think about such issues.

Problem is - while these will be resolved (in one way or another) - or left unresolved, as the user will only test the app on his device and that LLM "roll" will not have optimizations for the broad range of others - the user is still pretty much left clueless as to what has really happened.

Models theoretically inform you about what they did, why they did it (albeit, largely by using blanket terms and/or phrases unintelligible to the average 'vibe coder') but I feel like most people ignore that completely, and those who don't wouldn't need to use a LLM to code an entirety of an app regardless.

Still, for very simple projects I use at work just chucking something into Gemini and letting it work on it is oftentimes faster and more productive than doing it manually. Plus, if the user is interested in it, it can be used as a relatively good learning tool.

Re: AI will make formal verification go mainstream

#270

Post by blub »

gizmo686 wrote: post #211
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…

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…

> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity.

To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code.

However, even that weaker claim hasn’t been proven.

In my experience, the more information is encoded in the type system, the more effort is required to change code. My initial enthusiasm for the idea of Ada and Spark evaporated when I saw how much ceremony the code required.

Post reply on HN