[xavxav]

That’s my long term plan, I’d like to build something like Frama-C (https://frama-c.com/) but for Rust, but verification tools are not like other development processes and it’s not easy to piece them together.

I think that the first step is to develop a shared specification language for Rust, one that eventually could even become official like SPARK for Ada, then we move forward on integrating tools into a platform.

[touisteur]

Are you aiming to translate to Why3 like SPARK and Frama-C?

[xavxav]

I already do, my tool produces WhyML modules from Rust crates. But we can leverage Rust's ownership typing to drastically reduce proof obligations related to pointers and memory.

Incidentally, I've started working on a VSCode frontend to Why3 to replace the existing GTK one (https://github.com/xldenis/whycode), I'm currently rewriting the PoC as an LSP extension.

More broadly in the context of a Frama-Rust, much like Frama-C Why3 would be one of many possible backends. I specifically want abstract interpreters, test generation and other analyses to integrate and co-operate to solve proof obligations.

Ie: abstract interpretation could infer a loop invariant which is then used by a deductive backend to prove the function contract. Or a deductive failure could produce a counterexample which is transformed into a test case automatically.

[touisteur]

That looks amazing. You should shoot an email to Yannick Moy! He had lots of insights and ideas on how to help automatically generate or infer (reliably) loop variants/invariants (they use loop unrolling for example: https://blog.adacore.com/proving-loops-without-loop-invarian...) .

I know AdaCore uses CodePeer (abstract interpretation and iirc 'interval propagation') to help SPARK avoid or simplify some VCs and it helps in a lot of cases.

There's also some possibilities with symbolic execution, maybe on the counter-examples generation side.

I think you're treading a very interesting path!

[xavxav]

I've talked to Yannick quite a lot in the past as my lab develops Why3 and SPARK uses my translation for their new support for pointers (access types).

Additionally, my advisor collaborates with them on counterexample generation, especially with managing to get readable counterexamples out from the SMT. We've toyed a little with invariant generation but its very tricky to get something actually usable. Additionally, I have the personal (soft) requirement that the generated invariant should be injected into the source code and not purely internal / hidden.

[yannickmoy]

I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK!

Your plans for having Rust analyzers collaborate look very cool! Like you said, the first challenge is to agree on a base specification language. I hope this gets discussed at the next Rust Verification Workshop.

[touisteur]

Hi Yannick. Good to see so much collaboration in the FM world.