Graphiti
Verified graph rewriting system for dataflow circuits.
Lean 4 framework for verified graph rewriting targeting dataflow circuits. Rewrites are formally proved correct in Lean; an oracle component (Rust) handles matching. The codebase is structured into a reviewed core library, per-project modules, and an experimental area. It reads and writes Dynamatic-compatible DOT graphs and emits a JSON log of every rewrite step.
CompilerFormal MethodsHardware
- Technical
- Source code: Lab GitHub
- Last commit: 2026-03-19
Verification and Computer Architecture Lab
Verification and Computer Architecture Lab
Our research lies at the intersection between programming languages and computer architecture.
We are interested in designing high-level hardware programming languages especially to ease hardware verification. We leverage interactive theorem provers to reason about hardware, leading to more scalable and compositional proofs.
We also focus on building novel hardware architectures to support fine-grained and dynamic parallel computations.
We are interested in designing high-level hardware programming languages especially to ease hardware verification. We leverage interactive theorem provers to reason about hardware, leading to more scalable and compositional proofs.
We also focus on building novel hardware architectures to support fine-grained and dynamic parallel computations.
This page was last edited on 2026-03-19.
This page was last edited on 2026-03-19.