upload big files to Zenodo using cURL, jq and bash

The Scala 3 compiler, also known as Dotty.

Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

MLsem VS Code extension

Coq'Stats is a program to get statistics about Coq projects

⏰ AI conference deadline countdowns

mimalloc is a compact general purpose allocator with excellent performance.

The MLscript programming language. Functional and object-oriented; structurally typed and sound; with powerful type inference. Soon to have full interop with TypeScript!

Pandoc filter for cross-references

Rust bindings for the Z3 solver.

egraphs + datalog!

Coq plugin for extracting Rust code

An extremely fast Python package and project manager, written in Rust.

Some benchmarks of different languages

Licorne is an experimental programming language exploring refinement types and language-based support for lightweight verification

Lightweight coding agent that runs in your terminal

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

If T: Benchmark for Type Narrowing

"Trust no one, bench everything." - sbt plugin for JMH (Java Microbenchmark Harness)

https://openjdk.org/projects/code-tools/jmh

Semantic Type Soundness in Lean 4

the WebAssembly partial evaluator

Landing page for capture checking.

Experimental compiler for capybara.

Invariant Generation as Type Inference with GADTs and Existentials

Programming Language designed for Program Synthesis with SMT-validation.