Happy to chat about it. I looked at Aeneas, but as described, it only supports safe Rust. I also need C support so I can prove both the C and Rust code
Right now, I wrote a compiler that takes C and Rust code and compiles it to Lean. Then I have an LLM write a proof that the C and Rust code behave identically. I've been able to prove equivalent behavior for about ~70k lines of C code with pgrust.
The issue I've started to encounter is that the context needed for each incremental proof has kept growing, and things have slowed down dramatically. My hunch is that the speed is the time it takes to prove a line of code is on the order of O(n^2) of how much you've proved so far
I'm looking to see if there are ways to shard things so the required context scales better. Today I was going through the formal verification work Anthropic and Theorem published a few days ago, and it looks like they used some sort of orchestrator to manage all their proofs and ensure good clustering of similar code. I'm seeing if I can get an approach like that to work
It's just difficult enough that I think it's doable if done right. Half of me is debating if I should wait until the next model release because any improvement in model performance will help a ton
> I wrote a compiler that takes C and Rust code and compiles it to Lean
What if there are bugs in this C,Rust->Lean compiler? Anthropic are able to sidestep this by reasoning at the RISC V level for which its easier to develop a correct semantics.
My goal isn't to "prove" the software is correct. My goal is to find as many bugs as I can with the least effort. If I'm able to find all differences in behavior between pgrust and Postgres, sans bugs in the compiler, that's a real win for me
fwiw, I wouldn't say working at the assembly level solves the problem. You now need to make sure that your definition of the assembly behavior is correct