Hi everyone !
I recently started my PhD, the main topic of which is the verification of Rust programs. To clarify what it is, what it isn't and how my work will interact with other efforts in that area, I've written a blog post that explains it all to Rust programmers.
During a case study, I fixed a Servo bug using formal methods, I hope this method of bug-fixing will be more frequent in the future 
I am not a formal methods guy, but your blog post is so well written that I look forward to reading your thesis.
Hi,
I love this and have been waiting/hoping for deductive verification in Rust for a while!
A few questions more or less specific to your subject:
Does F* support proving properties about concurrent/parallel programs?
If not would this require temporal logics like CTL*?
Do any of the existing verification techniques you mention in your blog post support parallelism or concurrency?
Why does F* have/need header files?
How compatible is F* with Rust code? I've heard of KreMLin which translates Low*, a subset of F* to verified C code, however it has several limitations, such as (correct me if I'm wrong) non-recursive datastructures.
Thanks for your time and efforts!
Best,
ambiso
Unfortunately I think something happened to your blog. The post link consistently fails for me with ERR_CONNECTION_REFUSED (and I'm not having trouble with any other sites atm).
Yeah, clearly it's down i confirm... Some verified software failure here 
This is pretty cool !
I like that you started by introducing example-based unit tests and then went on to introduce the formal verification methods. As I typically use all example based tests, property-based tests, test mutation and fuzzing in production code - is there a good comparison I could read somewhere between these approaches and the formal verification ? I'm especially interested in effort vs number of bugs uncovered research, if there is any.
I typically write example-based tests to sketch out the program, then make them more generic and they become property-based and then I use fuzzer or mutation engine to uncover unknown properties and then encode them as proper property-based tests. I wonder how the workflow would look like using formal verification as well ?
Anyway, thanks so much for this effort again
@cyplo, Your testing process sounds both interesting and effective! Have you posted in detail about this process anywhere (or know of pointers to resources covering the process you use)?
Thank you I haven't posted about the workflow much to be honest, it's just something that I'm used to doing at work I guess. Happy to answer any specific questions - feel free to DM me here or on Twitter(@cyplo) - happy to jump on a call if needed as well
Hi ! Thanks for your interest. I'll answer to your questions :
F* does not support concurrent programs for the moment. There are several techniques to handle this in a verification logic. Rustbelt does it with a concurrent separation logic framework called Iris (https://iris-project.org/), and Viper also uses concurrent separation logic rather than CTL*.
F* has header files (.fsti) in the style of OCaml to be able to hide implementation details to other modules. Indeed, sometimes it can be useful to hide these details to the prover in order to not pollute the proof context.
Indeed, Low* is very limited and does not support recursive data structures. But neither does Rust (to declare a recursive data structure you have to Box or Rc the leaves for instance). The question of translating some kind of subset of F* to Rust is undecided at the moment, but this subset is likely to be as small as Low*, simply because F* don't support expressing difficult concepts of C or Rust.
Hi ! Thanks for your message.
Your testing process sounds very professional and exhaustive, and I'm sure that the code quality that results reaches very high standards already.
I would say that formal verification does not fit well in a model where you could have these sort of "effort vs number of bugs uncovered" statistics. Indeed, proving a property about a program can be very time consuming or very easy, and it's almost impossible to know in advance how difficult a proof will be (if it were, mathematics would be way easier). To get a glimpse into what the workflow would look like, you can check out this case study of mine : Rox* stories #1. But you do have to think about which property you want to prove about the program, so in your workflow you could try to prove some of the properties of your property-based tests.
If you manage to pull it off (which is not what typically happens to formal verification software) it will be a game changer. Good luck with your efforts and please try to foster the community that will help you with actually writing the code - too often what is left is a thesis and some proof-of-concept code completely unsuitable for industry use
Awesome stuff, thanks for that @denismerigoux - looking forward to the results
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.