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

421–430 of 448 posts

Re: AI will make formal verification go mainstream

#421

Post by antonvs »

astrostl wrote: post #169
roadside_picnic wrote: post #62

Earlier quoted context omitted.

I very much agree, and believe using languages with powerful types systems could be a big step in this direction. Most people's first experience with Haskell is "wow this is hard to write a program in, but when I do get it to compile, it works". If this works for human developers, it should also work for LLMs (especially if the human doesn't have to worry about the 'hard to write a program' part). > The next step up…

This is why I use Go as much as reasonably possible with vibe coding: types, plus great quality-checking ecosystem, plus adequate training data, plus great distribution story. Even when something has stuff like JS and Python SDKs, I tend to skip them and go straight to the API with Go.

Go has types? I didn’t notice.

Re: AI will make formal verification go mainstream

#422

Post by fulafel »

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…

This is the article's message as well:

"That doesn’t mean software will suddenly be bug-free. As the verification process itself becomes automated, the challenge will move to correctly defining the specification: that is, how do you know that the properties that were proved are actually the properties that you cared about? Reading and writing such formal specifications still requires expertise and careful thought. But writing the spec is vastly easier and quicker than writing the proof by hand, so this is progress."

General security properties come to mind as one area that could have good reusability for specs.

Re: AI will make formal verification go mainstream

#423

Post by signa11 »

amw-zero wrote: post #411
signa11 wrote: post #221

Earlier quoted context omitted.

> When you go to write a line of code, how do you decide what to write? depends ofcourse, what am i writing for ? a feature, a bugfix, refactor ... ?

Let's say a new feature. Do you just type random letters, or do you have some kind of plan ahead of time?

new feature implies design document to gather the thoughts, followed by an intense review etc.

Re: AI will make formal verification go mainstream

#424

Post by mdnahas »

andy99 wrote: post #36

Maybe a stupid question, how do you verify the verification program? If an LLM is writing it too, isn’t it turtles all the way down, especially with the propensity of AI to modify tests so they pass?

Yes, you’re right, it is turtles all the way down. But, a huge part of the prover can be untrusted or proven correct by a smaller part of the prover! That leaves a small part that cannot prove itself correct. That is called the “kernel”.

Kernels are usually verified by humans. A good design can make them very small: 500 to 5000 lines of code. Systems designers brag about how small their kernels are!

The kernel could be proved correct by another system, which introduces another turtle below. Or the kernel can be reflected upwards and proved by the system itself. That is virtually putting the bottom turtle on top of a turtle higher in the stack. It will find some problems, but it still leaves the possibility that the kernel has a flaw that accepts bad proofs, including the kernel itself.

Re: AI will make formal verification go mainstream

#425

Post by mdnahas »

I’m the author of a tutorial on Rocq.

I’m surprised at the negativity on HN. We all want bug-free code and this is a way to not just reduce bugs, but eliminate whole classes of bugs.

Moreover, with proven code, we can have rock-solid libraries and code reuse.

Also, proven specifications allow LLMs to do divide-and-conquer when generating code. You can ask it to generate part A that does X, assuming part B will do Y. And then ask it to generate part B in parallel. And know that, when merged, the code will work.

And, provable code is good for LLMs because it will let LLM creators study hallucinations. The proof checker can identify what is a hallucination and what is not. This means LLMs may learn what they don’t know!

I’m not saying LLMs with proven code is nirvana. There are parts of systems where it doesn’t apply. Specifications are often complex and difficult to understand. Some important details are hard to write a spec for. And specs can miss things. But code proven correct by LLMs has potential to do real good.

Re: AI will make formal verification go mainstream

#426

Post by pron »

igornotarobot wrote: post #323
mrkeen wrote: post #240

Earlier quoted context omitted.

Can TLA+ prove anything about something you specify but don't execute?

TLA+ is just a language for writing specifications (syntax + semantics). If you want to prove anything about it, at various degrees of confidence and effort, there are three tools: - TLAPS is the interactive proof system that can automate some proof steps by delegating to SMT solvers: https://proofs.tlapl.us/doc/web/content/Home.html - Apalache is the symbolic model checker that delegates verification to Z3. It can p…

> It may sound like executing your specification, but it is a bit smarter,

It's more than just "a bit smarter" I would say, and explicit state enumeration is nothing at all like executing a spec/program. For example, TLC will check in virtually zero time a spec that describes a nondeterministic choice of a single variable x being either 0 or 1 at every step (as there are only two states). The important aspect here isn't that each execution is of infinite length, but that there are an uncountable infinity of behaviours (executions) here. This is a completely different concept from execution, and it is more similar to abstract interpretation (where the meaning of a step isn't the next state but the set of all possible next states) than to concrete interpretation.

Re: AI will make formal verification go mainstream

#427

Post by amw-zero »

signa11 wrote: post #423
amw-zero wrote: post #411

Earlier quoted context omitted.

Let's say a new feature. Do you just type random letters, or do you have some kind of plan ahead of time?

new feature implies design document to gather the thoughts, followed by an intense review etc.

So... a specification.

Re: AI will make formal verification go mainstream

#428

Post by signa11 »

amw-zero wrote: post #427
signa11 wrote: post #423

Earlier quoted context omitted.

new feature implies design document to gather the thoughts, followed by an intense review etc.

So... a specification.

no ! a _design_ document. how this new thing will fit together with other things that are already existing in the system. what it’s interactions are going to look like, what are the assumptions, what are the limitations etc etc.

Re: AI will make formal verification go mainstream

#429

Post by Shocka1 »

kreetx wrote: post #256
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…

Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.

Piggybacking off your comment, I just completed a detailed research paper where I compared Haskell to C# with an automated trading strategy. I have many years of OOP and automated trading experience, but struggled a bit at first implementing in Haskell syntax. I attempted to stay away from LLMs, but ended up using them here and there to get the syntax right.

Haskell is actually a pretty fun language, although it doesn't fly off my fingers like C# or C++ does. I think a really great example of the differences is displayed in the recursive Fibonacci sequence.

In C#:

    public int Fib(int n)
    {
        if (n
In Haskell:

    fib :: Integer -> Integer
    fib n
      | n
As you might know, this isn't even scratching the surface of the Haskell language, but it does a good job highlighting the syntax differences.

Re: AI will make formal verification go mainstream

#430

Post by AlienRobot »

suspended_state wrote: post #390
TimTheTinker wrote: post #377

Earlier quoted context omitted.

> 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…

>an error of translation from natural language to formal language

Really? Programming languages are all formal languages, which means all human-made errors in algorithms wouldn't be "bugs" anymore. Some projects even categorize typos as bugs, so that's a unusually strict definition of "bug" in my opinion.

Post reply on HN