HN

Comments (43)

• Menu

  dfabulich
  Formal 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 verification boundary. Verification makes the core airtight but doesn’t guarantee end-to-end correctness.So you can formally prove that your e-commerce refund management logic is correct, except for proving that you processed the refund. You can't even prove anything about recording the refund in your database, say nothing of proving anything about your interactions with your payment processor.If your app is mostly tricky logic with just a bit of I/O, your app is very unusual, and it's almost certainly not an e-commerce app. E-commerce apps are mostly CRUD apps; I/O with the database, the UI, and third-party APIs (e.g. payment processors) is 99% of the code.Even property-based testing is mostly unhelpful for e-commerce apps like these.Instead, think of formal verification as a runtime performance improvement of property-based testing. If property-based testing is useful for your app (it probably isn't), then you may be able to convert some of your property-based tests into formal verifications.But, honestly, you probably can't do it, not even with a high budget of tokens.I'd love to be proven wrong, but the way to do it would be to formally prove the correctness of non-trivial open-source code with property tests. Perhaps you could formally verify significant chunks of Postgres! (But I doubt it.)
• Menu

  taeric
  I'm not entirely sure what this is showing people don't understand? Especially when going with such silly ill defined concepts as "financial conservation". Just what?Now model in that it was shipped, but an earthquake caused the delivery truck to be destroyed. Or it was shipped, but the person that ordered passed away before delivery and the estate is refusing to accept packages.People will want to somehow transfer the model of an online order as similar to an in store purchase. Does that mean that as soon as a customer takes an item through the door that the store is free of any and all obligations on the item?The answers in all of these will have to be that there are processes in place to be executed. Some may require overrides on state of execution that have to be applied to get things back to a resolved status.Now, do we want to make sure that normal execution of some code does not leave us in an unresolved status? Of course we do. And many people want to think they can find a way to model the world such that no contested states can exist. I have my doubts. But I welcome efforts to make it so that we surprise ourselves fewer times with some outcomes.
• GregDavidson
  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!
• thewillowcat
  I've been thinking about formal verification a lot, recently. I've dabbled in it before, but it was clear that it was only used by a small research community, and the effort required to verify anything larger than toy code would be immense. I agree with the author that there is enormous potential to use AI to automate the annoying parts of the verification process. What's more, the current security environment, in which the tiniest security flaw can quickly be exploited, suggests that provably secure code might be the future.Others are correct to point out that formal verification is too difficult to apply to many types of application code. But there are domains where it is applicable today, and the main reason it is not used there is that developers lack the time and know-how. For example, many file format parsers are exploitable, but they are simple enough that they could be formally verified.
• JacobAsmuth
  Anyone interested in this should check out my Qed project I've been working on, a formally verified web frontend. https://github.com/JacobAsmuth/qed
• Menu

  pron
  > It’s no longer just for safety-critical systems with the budget for specialized proof engineers. It’s for anyone who has a property worth proving... and the budget to pay the AI to prove it.I have quite a bit of experience with formal verification, but I don't understand the claim made in the article. As an aside, AI's ability to reliably prove the correctness of significantly large programs is still theoretical at this point, but let's assume it's possible. The claim in the article is that writing 10,000 lines of proof to prove a 100-line program was very expensive, and that's why it isn't done. But this increase in cost continues with AI! Whether you pay people to write the proofs or you pay an LLM to write the proof, you still have to pay for it. If I run a software company, saying that "verificaton is the AI's problem" isn't much different from saying, "it's the engineers' problem." Either way I'm not doing the work myself, but I am paying for it.If the premise is that writing proofs was 100x more expensive than testing, I see nothing in this article to even suggest why it wouldn't still be 100x more expensive when an LLM is doing the work.(BTW, the reason there aren't many specialised proof engineers is because they aren't in high demand; they're not being paid that much more than other engineers at a similar level)
• expo98
  I had fun in a college class that used Dafny, building a pseudo digital wallet, it wasn't the main focus of the class, so didn't get that much out of it
• hirvi74
  That there are bugs in it. That would be the only thing I can 100% guarantee.
• jongjong
  "The proof was only as good as the spec." Is the sentence which will go on the tombstone of Formal Verification.The spec has always been the problem. Whether the flaws in the spec arise from the customer or from the developer filling in the gaps in the spec incorrectly.If I built an entire system and the spec does not mention access control logic, then formal verification will neither prove nor disprove that the software is secure. It's just not in the spec...You have to know exactly what security properties you want. By the time you've written them down succinctly and correctly as a spec, you might as well have written them down succinctly and correctly as code.The spec has to be just as detailed and will be just as error-prone as the code itself.
• Menu

  03284782470
  ACM now stooping to the level of clickbait youtubers. Just great.
• Ozzie-D
  [flagged]