ztatlock
A zebra with sunglasses and laser eyes spelling Z.

Current Projects

egg

Fast and flexible e-graphs for optimization, synthesis, and verification

Ruler

Automatically inferring rewrite rules by and for equality saturation

FPBench

Numerical benchmarks, tools, and standards

Herbie

Automatically improving numerical accuracy

Carpentry Compiler

Synthesizing and optimizing carpentry build plans

Incarnate

PL tools and techniques for 3D printing

Past Projects

TVM Relay

Functional compiler IR for machine learning

Icing

Formally verified, accurate fast-math optimizations

Titanic

Number system design tools

Proof Engineering

Building and maintaining large verification efforts

Œuf

Correctly compile Coq in Coq via CompCert

Distributed Components

Modular verification of distributed systems

Cassius

Automated reasoning for web page layout

Herbgrind

Dynamic binary analysis for numerical error

Neutrons

Verifying safety of radiotherapy controls at CNTS

Verdi

Verifying distributed systems implementations

SpaceSearch

Formally verified solver-aided tools

Bagpipe

Formal verification for BGP router configurations

Peek

Extensible, formally verified peephole optimization framework for CompCert

Roboflow

Visual robot programming framework

Jitk

Formally verified BPF JIT compiler for Linux via CompCert

Reflex

Formally verified reactive programming framework for system shims

SafeDispatch

Compiler-enforced VTable hijacking defenses

Quark

Formally verified web browser kernel

Peggy

Emergent loop optimizations via equality saturation and PEGs

PEC/XCert

Extensible, formally verified optimizations via parameterized translation validation

Quail

Deep typechecking and refactoring for embedded DB queries in Java