Artifact generator for the paper "Incremental Forward Reasoning for White-Box~Proof~Search"

Can I make an *optimizing* compiler under 1k lines of code?

definition of coinductives types (M-types and indexed M-types) in Lean4, and some utilities for reasoning

Trying to do existential proofs with coinductive values.

A Lustre compiler in Coq

Relation algebra library for Coq

My TeX build system

Mechanized proofs and example programs for the paper Type Inference Logics, published at OOPSLA24.

Tiny verified SAT-solver

Timesec: a static analysis tool to sounldy prove timing side-channel freedom over a set of sensititve input variables for C functions

Recent symbolic execution papers and tools.

The proof systems used by Mina

Ascend - simple, yet fun terminal RPG.

A verified(?) TCP client/server chat application

Turn Python scripts into handouts with Markdown and figures

k/simple is a bare minimum k interpreter for learning purposes by arthur whitney

gpt written in plain c

SQL formal semantics with some extensions

PyXAI (Python eXplainable AI) is a Python library (version 3.6 or later) allowing to bring formal explanations suited to (regression or classification) tree-based ML models (Decision Trees, Random …

A small C compiler

Cryptographic protocol analysis for real-world protocols.

A powerful and user-friendly binary analysis platform!

Toy autograd engine in OCaml with Apple Accelerate backend

Mini egglog in Python

A simple BDD library for OCaml