Coq-of-rust: Formal verification tool for Rust
22 comments
·March 14, 2025SAI_Peregrinus
Animats
It's very useful for things where the specification is much simpler than the implementation. Databases and file systems are good examples. A database can be specified as giant arrays with linear search. Now prove that the database with all its optimizations and concurrency behaves the same as the simple spec.
null
SubjectToChange
Using (formal) specification languages doesn't guarantee a specification is "correct" either.
You have to write more code, and in a different language, but unlike just testing you can actually prove that invariants hold for all possible inputs.
Formal verification is needed to show that the code actually implements a specification. If anything, a formal specification is really good for generating test suites for the implementation code.
null
amw-zero
You are describing "validation": the process of verifying that your spec really says what you mean.
yodsanklai
I learned recently that the Coq project was renamed Rocq https://rocq-prover.org.
lelandfe
Not even a wink or a nudge about why they renamed: https://rocq-prover.org/about#Name
SubjectToChange
The linked discussion is upfront about the name change, if it wasn't already obvious.
https://coq.discourse.group/t/coq-community-survey-2022-resu...
lelandfe
Ah, the community voted on it. The reason why the survey was proposed shall, however, remain a mystery.
rafram
Probably the right move.
bigstrat2003
Definitely not the right move. The old name was perfectly fine and allowed for harmless fun. They can obviously do what they wish, but IMO there's no good reason to destroy good clean fun just because it might upset the occasional person.
jedisct1
Do that for Zig.
arn3n
Rust’s “mutable-xor-aliased” model makes it particularly amenable to developing verification tools on top of it [1]. Without this model, verification becomes just as hard — and just as practically intractable — as all the verifiers for existing languages.
johnisgood
> Rust supports it better than many other imperative systems languages -- even some impure functional ones!
I am surprised that this blog post does not mention Ada / SPARK at all though.
gaugefield
While this does not mention it, in many other discussions Rust vs Ada is mentioned. My (late) introduction to Ada via was finding out in one of the Rust forums.
> Even if Rust's type system prevents many mistakes, including memory errors, the code is still not immune to vulnerabilities, such as unexpected panics or wrongly implemented business rules.
> The way to go further is to mathematically prove that it is bug-free: this is named "formal verification" and what coq-of-rust proposes! This is the only way to ensure your code contains no bugs or vulnerabilities, even against state-level actors .
I like formal verification. But I consider this a misrepresentation of what it offers. It lets you mathematically prove that your code implements a specification correctly. It doesn't prove that your specification is bug-free & vulnerability-free. It doesn't prove that your specification correctly implements your business rules.
Formal verification is still extremely useful. It's often much easier to use a specification language to define invariants your programming language code needs to obey than to only implement things in a programming language. To me that's a much better, more honest selling point for formal methods. You have to write more code, and in a different language, but unlike just testing you can actually prove that invariants hold for all possible inputs.