alt Hacker NewsMy first question was “How do they know the proof correctly corresponds to the software they are checking?”
They say “ While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are: The formal models of RISC-V and of Linux processes;
The exact theorem statements that were proved;
The Rocq proof checker itself.”
What are the formal models of RISCV and Linux? I’m guessing they allow translation of RISCV code directly into Rocq proofs?
I’d love to see more info about their workflow of code -> proof. Or even an open source tool
Replies
Model: https://github.com/theorem-labs/rocq-linux-process-semantics based on https://github.com/mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: https://theorem.dev/oss-verify/ , https://github.com/theorem-labs/oss-verify , https://github.com/theorem-labs/oss-verify-proofs
You could search “decompilation into logic.”
Exactly. How do they now that the spec that was generated was correct? Is the spec also AI generated, and could the models lie to make a spec they can verify, just like they lie to make tests pass?
It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.
It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.