Comment by malisper
8 hours ago
For 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.
Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.
In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.
A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].
[1]: https://prela-lang.org/
[2]: https://github.com/remysucre/prela/tree/sqlstorm
[3]: https://github.com/remysucre/prela/tree/doom/
> In general, the spec must be human readable, and I believe to achieve that we must do away with SQL
Eh. Carthago delenda est? Why?
Yeah, that's the most impractical part of the original post.
Like, SQL was around before I was born, and barring the immanence of the Machine God (and potentially even then), will be around long after I die (unless civilisation collapses, I guess).
> 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
> How do you verify this compiler is correct?
I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it.
Did you consider using an established Rust verification toolchain like Aeneas?
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
1 reply →
Have you heard of Aeneas? In case you did, what are your opinions on it? Specifically, why you didn't choose it for your project.
From what I can tell Aeneas only supports safe Rust. I need something that works with both C and unsafe Rust.
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
Thanks!
I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.
I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.
What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.
Which models do you see to be productive for the task of writing lean? Big fan of pgrust.
I've been using Opus 5.5 for pretty much everything
I tried giving Astra a shot. Since it scores better on math, I thought it might do better at writing Lean. I forgot the exact details, but that didn't end up being the case. I think it wasn't thinking holistically enough and tended to rabbit hole itself more
Opus 5.5 is a god tier model, but for serious large scale work, nothing beats getting at least three non-similar models to repeatedly refine a super detailed plan before any code is written.
Right now my consortium is Opus 5.5, Grok 4.7 and Muse Wonder. These three are different enough that their insights are very complementary. Once a plan is detailed enough, any decent model can execute on it successfully, but I personally like Grok’s ability to stick to the plan. (And no 5-hour quota!)
3 replies →
Same experience on my vibe coding side project. Astra seems autistic to the context, Claude seems more of an open minded partner with good taste.
So far, I've proven that about 12% of the code behaves the same when executed single-threaded.
Dude, this is a database.
Concurrency is the source of all the hard stuff in databases.
Databases without concurrency are super-trivial.
I don't see any fundamental limitation that would prevent this from scaling up further.
The fact that you've dodged all the hard stuff is a pretty fundamental limitation.
Proving the code works single threaded is a stepping stone to eventually proving the code works under concurrency. It may be surprising, but very little of the Postgres code deals with concurrency. For the most part they've isolated the parts that deal with concurrency to a small number of subsystems. At least by volume of code, the vast majority of it is single threaded
the code is either single threaded or multi threaded. not partially...
so either you verify the whole thing or basically you didnt verify anything.
remember what verification is for. its great your query parser is functionally correct but verification is meant to prove something.
say you have a car. and its got safety requirements. those need to be verified. But now they say we've verified its safe only for the rear seat passengers. or, only the engine block is verified itll keep running safely.. it completely negates what is being done if its not done completely to the entire car.
and then ofc another driver just prangs into you anyway with their uncerified car, or suddenly the unverified road (OS) turns into a sinkhole and all ur verification still goes out the window..
there are limits already to verification if done properly and skipping the hard/important parts is really a big issue... u might aswell not do it.
(i do respect that there is a road to fully verified, u wont slap out those 9 million lines in one go. but saying you're winning halfway through the race.... nope)