alt Hacker NewsFor those skeptical, I've had decent success using formal verification for my Rust rewrite of Postgres. I wrote a compiler that can translate both Rust and C code into Lean. Once those two functions are in Lean, I have an LLM write a Lean proof that they behave identically.
So far, I've proven that about 12% of the code behaves the same when executed single-threaded. That works out to roughly 70k lines of C code. This has found very minor differences in behavior, such as how floating-point operations across platforms can produce different results.
I'm working on figuring out how to scale this up, but I don't see any fundamental limitation that would prevent this from scaling up further.
Replies
Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me
pgrust is incredible btw
Which models do you see to be productive for the task of writing lean? Big fan of pgrust.
> I wrote a compiler that can translate both Rust and C code into Lean
How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts