My 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
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