using lean to prove programs in other languages

Stream: new members

[Ayn]

Hello, I come across this paper https://www.usenix.org/system/files/osdi24-sun-xudong.pdf
And I was interested in the concept of proving the correctness of a program.
I was wondering if Lean can do same stuff, like prove other programs like C let's say

[Notification Bot]

A message was moved here from #new members > match with toLex by Ayn.

[Henrik Böving]

Yes there are multiple ways to verify programs not written in Lean with Lean, the three most common ones in increasing order of confidence in correctness:

• Formalizing a model of your algorithm in Lean, this is the technique the paper you linked uses. Note that this still relies on the fact that your algorithm is correctly implemented in your target language.
• Using differential fuzzing, you implement a version in Lean that you formalize and the actual version. Then you provide both versions with random inputs and check if they agree. Do this for a sufficient amount of inputs and you will get great confidence that your implementation does indeed behave the same as the verified one and thus most likely has the verified properties as well. This is for example how AWS verified Cedar in Lean.
• Actually formalize the semantics of your target programming language in Lean, read in the program and do reasoning about its semantics directly. Assuming that your semantics are correct this gives you basically absolute correctness confidence. This technique is very high effort and thus not employed often. One example of a high visibility project that did this is seL4 which was verified in this matter using Isabelle.

[Ayn]

Any pointers on how to start, I am both beginner in Lean and this "science?!"

[Henrik Böving]

Is there anything concrete that you wish to work towards?

[Ayn]

I just need to start with very basic stuff, proving correctness of something very straight forward, and gradually going into more complex cases, like concurrency and distributed systems

[Ayn]

also worth noting that my mathematical background is very limited as I am not a math grad, so something doesn't involve a lot of math sounds like a good starter

[Henrik Böving]

You can look into books like Theorem Proving in Lean 4 or Functional Programming in Lean 4 to get started. For material related to program verification you might want to check out the hitchickers guide to logic verification 2024.

Note that concurrency and distributed systems people have not yet started to do work with Lean so you will mostly be on your own if you wish to go into that precise direction.

[Ayn]

Thanks I will take a look at that

[Michal Wallace (tangentstorm)]

@Ayn if you don't have a specific C language program you want to verify, you could also start by just writing the program itself in lean. It's not "just" a proof language, and you can write and run programs without having to prove that they're correct.

In my (rather limited) experience, the verification part is much harder than the programming part, or at least requires a whole batch of new skills.

I wrote a simple prime number generator in lean in a couple hours, and have been working to formally verify it for about two three! weeks now... :) (I'm keeping a devlog in another thread if you're interested)

[Ilmārs Cīrulis]

If one wants to work with C language specifically, there's an option to use Coq and VST. I have done the first two Project Euler exercises using it... the third one was too hard for me, so it's postponed... :sweat_smile:

[Ilmārs Cīrulis]

Michal Wallace (tangentstorm) said:

In my (rather limited) experience, the verification part is much harder than the programming part, or at least requires a whole batch of new skills.

Completely agree...