kami

mit-plv/koika143

Hardware design language

A formal language for designing and verifying rule-based hardware systems

sifive/kami198

Hardware designer

A Coq-based DSL for designing and verifying hardware systems

sifive/prockami22

Processor simulator

Formal verification and implementation of RISC-V processor designs using Coq.

mit-plv/bedrock57

Program verifier

Automated verification of higher-order programs using separation logic

mit-plv/fiat149

Data type synthesizer

A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications

mit-plv/riscv-coq110

RISC-V spec

An implementation of the RISC-V instruction set specification in Coq

ml4tp/gamepad72

Proof platform

A platform that exposes Coq proofs to machine learning algorithms

mit-plv/coqutil42

Coq utility library

A collection of reusable tools and utilities for working with the Coq proof assistant

mit-plv/bbv27

Bit Vector Library

A repository unifying bit vector definitions and lemmas across multiple Coq projects.

vlsi-eda/poc554

Hardware library

Provides VHDL implementations of common hardware functions and a Python-based infrastructure for simulation and synthesis.

princetonuniversity/vst444

Formal verification toolkit

A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant

rdaly525/coreir101

Hardware compiler framework

Builds hardware descriptions into executable code using an LLVM-style compiler framework.

magmide/magmide810

Verification engine

Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers.

philtomson/rhdl14

Hardware description tool

A Ruby language and framework for designing and describing digital hardware systems