riscv-coq
RISC-V spec
An implementation of the RISC-V instruction set specification in Coq
RISC-V Specification in Coq
109 stars
15 watching
17 forks
Language: Coq
last commit: 4 months ago
Linked from 2 awesome lists
coq-community/awesome-coq
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 riscv/sail-riscv | A comprehensive formal specification of a RISC-V processor architecture using the Sail language | 461 |
| mit-plv/riscv-semantics | A formal specification of the RISC-V instruction set architecture in Haskell | 156 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 147 |
| mit-plv/bbv | A repository unifying bit vector definitions and lemmas across multiple Coq projects. | 27 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 50 |
 chipsalliance/riscv-dv | An instruction generator for RISC-V processor verification | 1,027 |
 mit-pdos/fscq | A file system written and verified in the Coq proof assistant with a focus on security. | 236 |
| mit-plv/kami | A platform for high-level parametric hardware specification and modular verification | 142 |
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 140 |
 huxpro/wasmcert | A formalized version of the WebAssembly specification using Coq | 21 |
 mrlsd/riscv-fs | A F# implementation of the RISC-V Instruction Set Architecture | 282 |
 riscv-mcu/riscv-openocd | A fork of OpenOCD with RISC-V microcontroller support | 34 |