Looks like an interesting project, though I would note they've just done the 'easy' part so far. As far as I can see it's base RV32I no CSRs, exception/interrupt support, PMP or other MMU. These are the features where the bugs tend to lie and also complicate your formal verification.<p>Still you have to start somewhere, I will be interested to see their progress as they tackle the things listed above.
The term "formally verified" could be misleading. Some people assume it means "100% bug free". Whenever someone claims something is formlally verified one should ask what properties were verified exactly. In this work the approach they use (bounded model checking) <i>could</i> find some bugs on a subset of RISCV archictecure they formalized. I recommend looking at their slides for better understanding of the scope of the work: <a href="http://www.clifford.at/papers/2017/riscv-formal/slides.pdf" rel="nofollow">http://www.clifford.at/papers/2017/riscv-formal/slides.pdf</a> Nevertheless it is definetely a very impressive work and pracrically useful.
I've been looking for an alternative hardware description language to Verilog/SystemVerilog because they're not very readable languages. But after skimming this source code, my initial thought is that I hope Haskell doesn't take off. This is extremely difficult to read.<p>Maybe I just don't know Haskell well enough, though.
So what kind of formal verification is it ? Is it proof assistant, model checking ?
And what does it verify ? It's not really clear from a first glance.
Hadn't heard of the VELDT board that this design targets, but it looks like it's based on the Lattice ICE40 which means you can use the open source yosys/symbiflow tools.