Hardware Verification

SailSail

A language for formally specifying instruction-set architecture (ISA) semantics with tooling for emulators, documentation, and verification.

Rapid Open Hardware Development (ROHD) FrameworkDart

A Dart framework for describing and verifying hardware, enabling modern software practices in hardware development.

F# RISC-V Instruction Set formal specificationF#

A formal and executable RISC-V ISA specification written in F# with a purely functional style, designed for clarity and reference.

RISC-V Specification in CoqRocq Prover

A formal specification of the RISC-V instruction set architectures (RV32I, RV64I) and extensions (A, M) written in the Coq proof assistant.

Mealybug Tearoom TestsAssembly

A collection of test ROMs for verifying Game Boy emulator accuracy, focusing on PPU register timing during rendering.

Bedrock Bit VectorsRocq Prover

A unified Coq library for bit vectors used across multiple MIT research projects.