I use formal verification as part of my development process. The needs of the proof guide the development of the code as much as vice-versa. The result is usually cleaner, simpler, smaller and usually more efficient programs developed much faster as debugging effort is minimal. I still create complete test cases. Proof maintenance as code changes is a pain and I would like LLMs and/or other tools to help with that. I would never try to formally verify code written with regular processes!
What can you confidently guarantee about your software?
41–50 of 71 posts
Re: What can you confidently guarantee about your software?
#42Earlier quoted context omitted.
Formal verification is a siren song. The siren sings, "bug-free code is possible in principle!" But it's a trap. Even with LLMs, bug-free code is impractical. I argued that property-based testing is mostly unhelpful for e-commerce/CRUD apps, and that formal verification is a performance improvement on property-based tests. In a property-based test, you identify some rule (an invariant) that you want to apply to your…
> It's already useful for many software platforms. It's useful for databases, where reliability is essential. It's useful for parsers, particularly when you expect the end user to be attempting to send you hostile code. > But e-commerce apps? So the e-commerce app doesn't use a DB? And the e-commerce app receives zero user input that needs to be parser so doesn't use any parser either? If you say its useful for, for…
Read carefully. There's a big difference between developing a database and developing an app that uses a database.
If you're developing a database, you should use property-based tests to ensure that your database behaves as expected (ACID reliability, etc.). If you can formally verify parts of your database, you won't have to fuzz it, because it will have been proven correct. But if you're developing a CRUD app that uses a database, there may be no properties of your app at all that are worth fuzzing.
Similarly, if you write a library that parses Markdown, you should write property-based tests of it, and fuzz it. If you use a library that parses Markdown, you should pass it your Markdown, and let the library handle it.
E-commerce apps typically don't need to do any non-trivial parsing. Effect-free logic is likely to be ~1% of your code base, or less.
This is why we keep talking past each other: the techniques that make sense for real-time operating systems don't make sense for an e-commerce app, a line-of-business admin dashboard, or a single-player game.
Re: What can you confidently guarantee about your software?
#43Earlier quoted context omitted.
> writing 10,000 lines of proof to prove a 100-line program was very expensive, and that's why it wasn't done. We are not that silly. We are writing compilers (ie model checkers) which translate the source code to formal proofs. No cost at all, you just need to limit loop sizes and function call depths, to keep the cost of the proof down. And then extrapolate the little proof to the general proof.
Whatever the cost multiplier is, I see no reason why that same multiplier won't remain with AI. Personally, I don't think that picture is quite accurate. Yes, there is a high cost multiplier for small programs , albeit perhaps not so prohibitive. But for large programs, that multiplier is, for most intents and purposes infinite, unless, perhaps , you have experts who know what's worth proving and what is not. Anyway,…
> Have an LLM write a 50-100KLOC program and prove all correctness properties [...] and tell us what it cost.
Assuming the 50-100KLOC program is of real-world use and not something contrived for the sake of offering something to prove, it is unlikely that proving all correctness properties will be possible, fundamentally. So costs will be nothing — or infinite if you foolishly remain determined to try the impossible.
In the real world we restrict what properties we care about and what models we reason in. Some of those models are woven into the fabric of an LLM. I would think the cost multiplier in those cases is much lower for an LLM as compared to a human that doesn't have an inherit understanding and needs to give it thought. Wouldn't you?
Re: What can you confidently guarantee about your software?
#44That there are bugs in it. That would be the only thing I can 100% guarantee.
Re: What can you confidently guarantee about your software?
#45Earlier quoted context omitted.
Whatever the cost multiplier is, I see no reason why that same multiplier won't remain with AI. Personally, I don't think that picture is quite accurate. Yes, there is a high cost multiplier for small programs , albeit perhaps not so prohibitive. But for large programs, that multiplier is, for most intents and purposes infinite, unless, perhaps , you have experts who know what's worth proving and what is not. Anyway,…
> Have an LLM write a 50-100KLOC program and prove all correctness properties [...] and tell us what it cost. Assuming the 50-100KLOC program is of real-world use and not something contrived for the sake of offering something to prove, it is unlikely that proving all correctness properties will be possible, fundamentally. So costs will be nothing — or infinite if you foolishly remain determined to try the impossible.…
> I would think the cost multiplier in those cases is much lower for an LLM as compared to a human that doesn't have an inherit understanding and needs to give it thought. Wouldn't you?
No. I don't see why proving would require less relative effort for an LLM. In fact, years ago, long before LLMs, I wrote about why it is relatively easy to write sort-of-correct software yet hard to write provably correct software, and I don't see why it's any different for LLMs. Their power lies in inductive "intuition", while deduction requires effort, just as it does for humans: https://pron.github.io/posts/people-dont-write-programs
But there's no need to speculate. Those who think verification-by-LLM is feasible and cost-effective on an industrial scale, are welcome to try it and report what they find. So far I've seen only tiny examples, and even they don't show effortless (i.e. token-light) work by the agent.
Re: What can you confidently guarantee about your software?
#46[flagged]
Re: What can you confidently guarantee about your software?
#47Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…
So much this. I actually did take a formal verification course in college. Our final project was to use the techniques we'd been learning to verify some classic critical-section locking algorithm. I chose to verify an implementation of Lamport's bakery algorithm[0] in C (this was the 90s -- a lot of code was still being written in C). The problem is that Lamport's algorithm makes an assumption that the "ticket number…
You shouldn't have been able to formally verify the algorithm fails to protect the critical section. Wrapping ticket numbers can lead to starvation (literally, if we follow the baker analogy), but the algorithm protects the critical section so long as thread IDs are unique.
The sort of environments in which this is a problem would be extremely uncommon. For a start, you need continuous contention. If you ever get a break in contention you no longer have starvation, and you 'reset' the ticket number monotonicity - to zero, if you actually take a maximum of entering thread ticket numbers instead of a cheap global counter.
If you do actually have an environment in which you expect to have continuous contention over a critical section, some quick napkin math can tell you if it's something to worry about based on the running time of your critical section. If it's over, say, 10ms, you've got a few years of runtime before it's a problem. If it's under 1ms, maybe you want to use 64-bit arithmetic for your ticket number so you can run your system until long after the human species is extinct.
You probably got a 'B' because you didn't give the professor the answer they expected, though, not because of any technical reasons.
Re: What can you confidently guarantee about your software?
#4860% of the time it works every time.
Re: What can you confidently guarantee about your software?
#49My professor was literally E. Allen Emerson (RIP) in uni so I feel like I'm in a unique position where the jab in the article title doesn't apply to me.
Re: What can you confidently guarantee about your software?
#50Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…
I have minimal experience with formal verification, but I’d be curious to hear your view on Deterministic Simulation Testing (DST) and how that slots in to the conversation.
That to me seems to address a lot of the IO facing pitfalls formal verification can struggle with. At the obvious cost of it being a bear to implement.