Alternative to frama-c to proove C++ formal verification:z3?

Stream: lean4

[D.E]

Hello.

I want to translate the internal of a C++ program into a modelisation of a studiable proof demonstration in order to make a thesis. I checked out frama-c. It is good but does not work with C++.

I checked out the tool z3 and according to this line, it seems it could be used as a wrapper to test values: https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp#L32 . It is not as perfect as frama-ci but it works for c++.

I am wondering if you knew a tool that could set annotation upon C++ function like C++17 with a good support please? Might it be possible with lean please?

Best regards.

[suhr]

I can't help you with C++, but I can recommend Creusot and VeriFast for verifying Rust code. There's also RefinedRust and in the future there will be also Gillan-Rust for hybrid safe/unsafe verification of Rust code.

Maybe rewriting it in Rust is not a bad idea after all.

[suhr]

I want to translate the internal of a C++ program into a modelisation

Wait, do you want to verify a C++ program or you want to analyze it yourself in some way?

[D.E]

Hi @suhr

The verifast devs disrecommend me the tool for C++ as not fully supported for each C++ version. creusot seems to be pure rust as verus.

I still hesistate between verifast and z3 wrapper to wrap my function manually. Thank you very much for your help. I really need to choose between these 2 tools.

[Mario Carneiro]

Note, this is a zulip instance for the Lean theorem prover, which is not really related to either of those tools and is solving a different kind of problem. Probably you would be best served asking this question elsewhere.

[Mario Carneiro]

Might it be possible with lean please?

No, lean does not do anything about C++ formal verification. You could in principle build such a tool but it would be a multi-year project.