Comment by m1el

I understand that formal verification is not panacea.

My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".

We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.

I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually:

    * Understandable
    * Portable across projects, you could imagine something like
        from specs import no_stealing_secrets
        no_stealing_secrets(secret_table)
    * Implicitly proves the absence of RCE, though I suppose
        it could allow something truly crazy like an interpreter
        that will run any attacker supplied program that can 
        be proven not to steal the specified secrets

Yes, this is a challenge, but I don't think it's as damning as it sounds.

First, the same kind of issue exists with any kind of testing. We all know that having unit tests and integration tests doesn't mean the software is correct and bug-free. Yet we still often believe it's worth investing in writing and maintaining a test suite. Formal methods is an additional level of assurance that I suspect we'd generally find worth it for critical software if it were easy enough to implement, even if it's not perfect.

Second, because formal verification has been so hard, nobody has really bothered making a serious attempt at solving the spec problem before (at least not to my knowledge). We've spent decades building frameworks that make writing tests really easy. We really have not come close to investing the same kind of effort into building frameworks and tools to make writing formal specs easy. I can imagine a world where we have sophisticated tools that help us create specs, plus real-time verification infrastructure that automatically reverifies code against the spec on each PR.

Third, and perhaps most importantly, there are many industries where this is actually low-hanging fruit: aerospace, medical devices, etc., actually already have formal specs that are verified manually by human engineers to satisfy certification requirements. I believe that's a more natural starting point vs. trying to scale formal methods for all software in general.

Of course, and correct verification assumptions were always a challenge, and they are a possible failure point - but 95%(?) of labour was then proving the code, and now that part can be largely automated.

Speaking of how difficult can it be to write a proper spec, I think a few years ago someone found a bug in spec in a helloworld-like example in a book about formal methods, and a bug in the code.

Just as an addendum to some of the other fine replies you've got, one of the things I'm interested in for formal verification is security assertions, and those don't necessarily need lots of comprehension to apply. If you can assert "this code never hits the network again" or "this code will never execute arbitrary code", the proof of that may be nontrivial but the comprehension of it is easy.

Proving that some complicated algorithm is actually what you think it is, even after you've proved that it does whatever it is it does, is hard. But to me, and me personally so not necessarily what everyone else thinks, that's not really what I'm interested in from proofs. I'm really more interested in these overarching declarations of what the code definitely doesn't do, or putting bounds on what it does, rather than proving that my billing code bills the customers precisely in the way I expect, when, frankly, the best specification of it I have is already what is in the unproved code base anyhow. I believe those have a very sensible story as to how both humans and AIs can use those assertions.

While that is true, just having LLMs "think about it" may discover unintended behavior and exploits, and you can choose to what extent you want to verify that the claims are correct.

The LLM does not prove anything (it cannot reason). It generates Lean code, and conveniently, in Lean, the code is also the proof. It’s not merely a model of the stated system, it is the system.

You still need to verify that the generated code is what you asked for, though.

> in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point

CPUs are tested so so much more thoroughly than any software today. Including using formal proofs.

If the chance of a CPU bug is something like 1/10^6 and each module in your software is 1/10, reducing that to 1/100 makes a bog difference.

Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties.

Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...