a heterogeneous reflective tower where level 0 is an exact Scheme-like interpreter and level 1 is an LLM

A modern, TreeSitter-powered, Emacs major mode for OCaml

Verified Verilog Equivalence checker, written and verified in Coq.

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

The rule-based graph programming language GP 2

KLEE Symbolic Execution Engine

List of awesome open source hardware tools, generators, and reusable designs

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

A minimal development of SSA theory

Opensource DDR3 Controller

Textbook and full source codes to learn basics of RISC-V pipelined CPU design using the Bluespec Hardware Design Language(s)

Minimal implementations for dependent type checking and elaboration

Focus: a minimalist presentation theme for LaTeX Beamer.

A Flexible and Efficient Proof Checker for SMT Solvers

130nm BiCMOS Open Source PDK, dedicated for Analog, Mixed Signal and RF Design. Documentation is here:

This package provides an interface and foundation for verified SAT reasoning

Analyze Rust crates without touching compiler internals

A verification toolchain for Rust programs

Ocaml Linear Engine for JavaScript Regexes, implementing the algorithms described in Linear Matching of JavaScript Regular Expressions at PLDI24

A simple DDR3 memory controller

A Foreign Function Interface (FFI) to cvc5 solver in Lean.

Tactics for discharging Lean goals into SMT solvers.

Source code for raintown.org website

Helper toolkit for creating your own Lean 4 UserWidgets

The "batteries included" extended library for the Lean programming language and theorem prover

Functional Hardware: FPGA synthesis from Haskell