diff --git a/docs/references.md b/docs/references.md
index dc2a358..9f3e447 100644
--- a/docs/references.md
+++ b/docs/references.md
@@ -6,10 +6,13 @@ ARM's [ISA-Formal Framework](https://alastairreid.github.io/papers/cav2016_isa_f
 
 Other RISC-V formal verification projects and related materials:
 
-- [Kami: A Framework for (RISC-V) HW Verification](https://riscv.org/wp-content/uploads/2016/07/Wed1130_Kami_Framework_Murali_Vijayaraghavan.pdf)
+- [Kami: A Framework for (RISC-V) HW Verification](https://riscv.org/wp-content/uploads/2016/07/Wed1130_Kami_Framework_Murali_Vijayaraghavan.pdf) ([kami on github](https://github.com/mit-plv/kami))
+- [Rewrite of Kami by SiFive](https://github.com/sifive/Kami)
 - [Verifying a RISC-V Processor, Nirav Dave, Prashanth Mundkur, SRI International](https://riscv.org/wp-content/uploads/2015/06/riscv-verification-workshop-june2015.pdf) ([l3riscv on github](https://github.com/SRI-CSL/l3riscv))
 - [RISC-V ISA Model in Bluespec BSV by Rishiyur S. Nikhil](https://github.com/rsnikhil/RISCV_ISA_Formal_Spec_in_BSV)
 - [RISC-V ISA Model in Haskell by Adam Chlipala and group (MIT)](https://github.com/mit-plv/riscv-semantics)
+- [RISC-V ISA Specification in Coq by MIT CSAIL](https://github.com/mit-plv/riscv-coq)
+- [RISC-V ISA Specification in Coq by SiFive](https://github.com/sifive/RiscvSpecFormal)
 - [RISC-V ISA specification work in Sail 2](https://github.com/rems-project/sail/tree/sail2/riscv)
 - [Sail: a language for describing instruction semantics](http://www.cl.cam.ac.uk/~pes20/sail/)
 - [riscv-fs: F# RISC-V Instruction Set formal specification](https://github.com/mrLSD/riscv-fs)