IMO the realistic path towards formal verification is AI proof assistants that automate the tedious parts instead of forcing you to write your code in a weird way that's easier to prove
But AI code generation for formally verifiable programs? And to assist in writing custom domain-specific verifiers? Now that's the sweet spot. The programming languages of the future, and the metaprogramming libraries on top of them, will look really, really cool.
For verifiable domains, this really is the sweet spot.
An annoying aspect of verification-in-practice is that it is just really bulky—there's a lot to type in, and it's tedious.
LLMs, especially the latest crop of weak-reasoning models, are great for this.
Only after telling it that I tested the code and that it works did it somewhat accept that the solution worked.
I think a deterministic, unambiguous process is a lot more valuable for formal verification.
[0] https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
In my experience, if I ask it to do web things in PHP or Java, data things in Python, ... it gives a good enough result. If I ask it a postgis question, I get an answer with hallucinated APIs, bugs, and something that doesn't even do what I want if it works.
I suspect the ADA/Spark world and the formal verification world are to small to decently train the AI.
Or to phrase it another way, there must examples of the technique that you want to "generate" in the training set otherwise the horrifically overfitted model cannot work.
Probably a little bit too cynical but this is my experience asking LLMs "unusual" questions.
I tried asking a LLM for a full code snippet for the first time yesterday (i've been using them as search engines better than google, which isn't saying much, before).
It produced code that compiled but failed to do anything because the 3rd api call it generated returned an error instead of doing what the LLM said it would do.
Didn't spend time on seeing what was wrong because we already had a library that did the same thing; I was more testing what the LLM can do.
I might consider AI if it utilised SPARKs gnat prove but I wouldn't usw AI otherwise.
At least that's what it should mean. It's not clear if that's going to happen.
I don’t really use AI tools, but in the past few weeks I’ve tried it with Rust and while it had problems, borrow checking errors were never part of them.
I fully agree that LLMs don’t “understand,” but people also really oversell the amount of thinking needed to satisfy borrowing in a lot of cases.
Is this true? There should always be a QA process and you should always carefully review when committing. The writing process doesn't influence that unless you're automating whole swaths you don't understand during reviews.
https://www.slideshare.net/slideshow/securing-the-future-of-...
I am rather skeptical of AI in this context. Until you have verifiably correct AI assistants, you still need a highly skilled human in the loop to catch subtle errors in the proofs or the whole result is moot anyway.
And there _are_ tools out there capable of verifying C code, but for a greenfield project implementation/verification in a higher-level, formal language + verified compilation might make more sense.
Their linked case study lists three examples and one category, https://www.adacore.com/uploads/techPapers/222559-adacore-nv...
- image authentication and integrity checks for the overall GPU firmware image
- BootROM and secure monitor firmware
- formally verified components of an isolation kernel for an embedded operating system
- In general, their targets tend to be smaller code bases that would benefit the most from SPARK’s strong typing, absence of runtime errors, and in some cases, rigorous formal verification of functional properties
> NVRISCV is NVIDIA’s implementation of the RISC-V ISA and Peregrine subsystem includes NVRISCV and multiple peripherals. They show how fine-grain access controls, formally verified for correctness, allow following the principle of least privilege for each partition. NVRISCV provides secure boot that starts with an immutable HW, the chain of trust extends to the Secure Monitor in SW, where partition policies are set up and isolation enforced using HW controls.. Boot and Secure Monitor software is implemented in SPARK.
That's the same paradigm as outsourcing development at some cheap place and doing acceptance tests against the result. It saves money but that's not how you'd build an airplane for instance...
Unless you want it going boing boing boeing.
Haha what?
What are you comparing this to?