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.

In this repository we simulate the semantics of the DC dialect with verilator and (1) compare it against the semantics we mechanize with Lean-MLIR (2) assess the verification efforts at Handshake v…

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

Interface with the rustc compiler for the purpose of program verification

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

A minimal GPU design in Verilog to learn how GPUs work from the ground up

Experiments on automation for Lean

Reed-Solomon Decoder

DHLS (Dynamic High-Level Synthesis) compiler based on MLIR

A tool to generate optimized hardware files for univariate functions.

An API built to enable one-line-of-code access to accelerated open-source and custom AI models.