Hello,
First of all, congratulations on extending the RISC-V verification down to the binary level! 
I see seL4 and RISC-V have formed an alliance of sorts, and I was just curious if you are cooperatively working on the formal ISA spec or is that entirely owned by seL4?
We are collaborating with the RISC-V foundation, and the ISA spec is controlled by RISC-V. I’m not entirely clear on who owns the official formal ISA spec in terms of copyright, but it’s definitely not the seL4 Foundation. I don’t think the binary verification project has influenced the ISA spec much, but there is another seL4 project running, about timing channels, where @gernot is having a lot of discussions with the RISC-V community about what the right mechanisms are.
We are currently actually not using the officially released formal spec (the project started long before that spec existed). This is mostly a tooling question. The official spec is written in the SAIL tool, the binary verification toolchain connects to a different tool, called L3. There are a few more variants of formal specifications for the RISC-V ISA out there. The main differences are in completeness and tooling, not so much in semantics.
The ISA subset we use is not that complex, so it’d be a nice project to see if we could get an automatic equivalence proof between the two specs for that subset, or maybe get SAIL to produce L3 input.
… or retarget our tool chain to SAIL There are some people interested in this, which could translate into funding, but that’s pretty vague at this stage.
As Gerwin says, the formal RISC-V spec (that’s now the primary spec, replacing the original informal spec) has been developed independent of us, the SAIL formalisation is Peter Sewell’s work. And yes, I’m working on getting the right mechanisms into the spec for complete prevention of microarchitectural timing channels (on-core channels for now).