[libre-riscv-dev] formal verification

[Hendrik Boom]

I've been wondering whether to voluntee here, because

* I don't have any hardware experience
* I haven't done any work in formal verification recently (but I was 
  developing a type-theory verifier three decades ago)
* I probably haven't the time to do it,
  * let alone time to get up-to-date on proofs about hardware
* And even if I succeed, waiting for me would delay the project 
  significantly
* And I do't know if the tools I can use are compatible with the tools 
  you use

but ...

would it be helpful if I were to look into formal verification of any 
of this RISC-V architecture under development?

And what do I need to get familiar with any of it?  (links to documents 
and software, please)

-- hendrik