"[..] the last time I taked to him about pgrust verification, he mentioned using Kani to verify some parts of the code. He's since switched to Lean and has been using Lean to verify things that are too complex to do in Kani. This would be another topic for another post,"

I'd love to read that post!

I understand how to use Kani. I suppose Rust with Lean involves Aeneas, but this is over my head. I'd love someone to write this up, not only the mechanics but also exploring the current practical limits of it.

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