Formal verification of LLVM?

Stream: Is there code for X?

[Xiyu Zhai]

There is a formal verification of llvm written in Coq <https://github.com/vellvm/vellvm/>. I wonder whether similar efforts exist in Lean. If not, I plan on writing a Lean version myself (first by translating vellvm), which would be a great way of learning both LLVM and formal verification.

[Mario Carneiro]

No, there isn't anything like that in lean. FYI LLVM is huge and I strongly doubt any claim that it's been formalized

[Mario Carneiro]

Vellvm is an ongoing project aiming at the formal verification in the Coq proof assistant of a compilation infrastructure inspired by the LLVM compiler.

[Xiyu Zhai]

Mario Carneiro said:

No, there isn't anything like that in lean. FYI LLVM is huge and I strongly doubt any claim that it's been formalized

You're right. Thanks a lot.

[Xiyu Zhai]

I think the great advantage of formal verification is that there is no need for debugging. So any code written is work done. Although LLVM is large, it's much easier to write in formal language than maintaining in C++. I believe in the future, people shall rewrite it using a language that can both do formal verification and also do system-level programming.

[Mario Carneiro]

You're speaking to the choir (I did a whole PhD on this topic), but when it comes to translating an existing large C++ project it's a very uphill battle. Before you could even prove anything you would first have to figure out what the invariants of the code are and why all that C++ code satisfies those invariants. This is an extremely hard problem in practice, because it is poorly documented and in many cases not well understood even by the authors of the code. Not to mention it's obviously untrue in some places, which is why there are bugs in it

[Mario Carneiro]

There is a reason vellvm is "inspired by" LLVM and not literally LLVM

[Xiyu Zhai]

Indeed. You're right. So I'm not eager to put C++ dominance to an end.

[Xiyu Zhai]

But I don't believe LLVM will be there forever. I'm thinking of Rust compilation, it's slow partially because of LLVM. I would argue that formal verification will (maybe taking many decades) eventually be an essential part of a future compiler framework.

[Xiyu Zhai]

My interests in this is to learn things and mature the design of my own programming language (for my PhD).

[Xiyu Zhai]

I just wonder which is more difficult, this or verify proof of Fermat's last theorem.

[Mario Carneiro]

That's a very interesting question. My money is on FLT being easier than LLVM

[Mario Carneiro]

but then again, CS projects often have more human capital to throw at the problem

[Xiyu Zhai]

Indeed. And there are more people known LLVM or can learn it than FLT. So hard to say.