Comment by sestep
8 hours ago
Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.
How do you gain confidence that your theorem actually applies to your code?
My Rocq setup directly reads my actual code. And I fuzz my semantic models against the real machine.
Is this closed source?
I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.
Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.
Does this require having a Rocq semantics of LLVM IR? Which one do you use?
2 replies →