Xavier Denis

ternlight. Python

Forte. An async-compatible thread-pool written in rust.

dial9. Tokio Telemetry you can run in production

ublock-hide-yt-shorts. Maintained - uBlock Origin filter list to hide YouTube Shorts

kmcuda. Large scale K-means and K-nn implementation on NVIDIA GPU / CUDA

KMeansRex. Fast, vectorized C++ implementation of K-Means using the Eigen matrix template library. Includes Matlab and Python interfaces.

kmeans. A CUDA implementation of the k-means clustering algorithm

napkin-math. Techniques and numbers for estimating system's performance from first-principles

garage. (Mirror) S3-compatible object store for small self-hosted geo-distributed deployments. Main repo: https://git.deuxfleurs.fr/Deuxfleurs/garage

cachey. Read-through cache for object storage

hermitage. What are the differences between the transaction isolation levels in databases? This is a suite of test cases which differentiate isolation levels.

synquid. Haskell

containerization. Containerization is a Swift package for running Linux containers on macOS.

afl.rs. 🐇 Fuzzing Rust code with American Fuzzy Lop

trc. A faster Arc.

turmoil. Add hardship to your tests

yap. Yet Another Parser library for Rust. A lightweight, dependency free, parser combinator inspired set of utility methods to help with parsing strings and slices.

kanal. The fast sync and async channel that Rust deserves

xlskubectl. xlskubectl — a spreadsheet to control your Kubernetes cluster

sanicdns. Gotta go fast

axum-htmx. A set of htmx extractors, responders, and request guards for axum.

md-lsp. Markdown language server

elf-shenanigans. Linker experiments

ghostty. 👻 Ghostty is a fast, feature-rich, and cross-platform terminal emulator that uses platform-native UI and GPU acceleration.

silicon. Symbolic-execution-based verifier for the Viper intermediate verification language.

diamond-lang. A prototype programming language with polymorphic reachability types that track freshness, sharing and separation.

arrow-rs. Official Rust implementation of Apache Arrow

soteria. Scaling Reasoning for the Age of AI

ekege. A different approach to an E-graph library

ERASan. LLVM

hol-light. The HOL Light theorem prover

ocaml. The core OCaml system: compilers, runtime system, base libraries

cc-lemma. Refreshing automation for inductive equational proofs using e-graphs

comp-gen. Automatically generate a compiler using equality saturation

creusot-ide. OCaml

nemo. A fast in-memory rule engine

roogle. A Rust API search engine

eggmt. Egraphs Modulo Theories

whisperX. WhisperX: Automatic Speech Recognition with Word-level Timestamps (& Diarization)

abont. Finally, a shell for all seasons!

alien. ALIEN is a CUDA-powered artificial life simulation program.

stellogen. An experimental language exploring computation and meaning through term unification, with logic-agnostic types.

knuckledragger. A Low Barrier Proof Assistant

boogie. A (not yet) complete implementation of a Boogie parser and pretty-printer

gearley. An Earley parser engine in Rust.

create-gh-release-action. GitHub Action for creating GitHub Releases based on changelog.

dyro. Dyro: Dynamic Rust Ownership Verification

fromthetransistor. From the Transistor to the Web Browser, a rough outline for a 12 week course

ante. A safe, easy systems language

fls. The FLS

VerifiedDBM. DBM Implementation Verified by Creusot

lady-deirdre. Compiler front-end foundation technology.

chumsky. [Chumsky has moved to Codeberg!] Write expressive, high-performance parsers with ease.

lelwel. Resilient LL(1) parser generator for Rust

a-mir-formality. a model of MIR and the Rust type/trait system

truck. Truck is a Rust CAD Kernel.

once_map. Single assignment and lazy maps

autoken. A rust-lang compiler tool adding support for automated borrow-aware context passing

bluefin-algae. Algebraic effects in the Bluefin effect system

FriendsDontLetFriends. Friends don't let friends make certain types of data visualization - What are they and why are they bad.

claude-cookbooks. A collection of notebooks/recipes showcasing some fun and effective ways of using Claude.

rust-peg. Parsing Expression Grammar (PEG) parser generator for Rust

faster-pest. A generator for high-performance Pest parsers, bringing your grammar to the next level

is-jonschlinkert. Returns true if a package is maintained by jon schlinkert

verifast. Research prototype tool for modular formal verification of C, Rust and Java programs

wtransport. Async-friendly WebTransport implementation in Rust

autoclave. repeatedly run programs until they break, and be ready to attach a debugger

macprefs. Command and library to export macOS preferences.

creusot. Creusot helps you prove your Rust code is correct.

plat-smt. Toy `QF_UF` SMT solver written in Rust

foundationdb. FoundationDB - the open source, distributed, transactional key-value store

erased_brand. Rust

salsa. A generic framework for on-demand, incrementalized computation. Inspired by adapton, glimmer, and rustc's query system.

viddy. 👀 A modern watch command. Time machine and pager etc.

why3-semantics. Formal Semantics for Why3

ferrocene. Source code of Ferrocene, safety-critical Rust toolchain

PAROL6-Desktop-robot-arm. BOM, STL files and instructions for PAROL6 3D printed robot arm

Big-Ass-Data-Broker-Opt-Out-List.

rfun-interp. Interpreter for the reversible functional language rFun

just. 🤖 Just a command runner

io. IO should be just a library

embassy. Modern embedded framework, using Rust and async.

Whisky. A modern Wine wrapper for macOS built with SwiftUI

abella. An interactive theorem prover based on lambda-tree syntax

uvm. Fun, portable, minimalistic virtual machine.

CompCert. The CompCert formally-verified C compiler

tree-beamer. Slides and sources for talks on Tree Borrows

unison. A friendly programming language from the future

eff. 🚧 a work in progress effect system for Haskell 🚧

effectful. An easy to use, fast extensible effects library with seamless integration with the existing Haskell ecosystem.

cleff. Fast and concise effect handlers

grasshopper. An automated deductive program verifier.

catty. A unikernel as an IRC client

ui_test. A test framework for testing rustc diagnostics output

koka. Koka language compiler and interpreter

effing-mad. Algebraic effects for Rust

HVM2. A massively parallel, optimal functional runtime in Rust

typst. A markup-based typesetting system that is powerful and easy to learn.

fast_expr. Fast expressions.

nola. Nola: Later-Free Ghost State for Verifying Termination in Iris

iina. The modern video player for macOS.

metrics. A metrics ecosystem for Rust.

c2rust. Migrate C code to Rust

VST. Verified Software Toolchain

flux. Refinement Types for Rust

nix-darwin. Manage your macOS using Nix

pixels. a shared pixel display controllable via TCP

vel. Vel: A language for verified low-level software

julius. An open source re-implementation of Caesar III

augustus. An open source re-implementation of Caesar III

vigil. Vigil, the eternal morally vigilant programming language

dolmen. Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

verus. Verified Rust for low-level systems code

AudioLab. Pure Data abstractions for electroacoustic composition & live electronics

aeneas. A verification toolchain for Rust programs

reminders-cli. A simple CLI for interacting with macOS reminders

diffusionbee-stable-diffusion-ui. Diffusion Bee is the easiest way to run Stable Diffusion locally on your M1 Mac. Comes with a one-click installer. No dependencies or technical knowledge needed.

cargo-careful. Execute Rust code carefully, with extra checking along the way

creusot-experiments. Rust

cdsat. OCaml

lambdapi. Proof assistant based on the λΠ-calculus modulo rewriting

lean4. Lean 4 programming language and theorem prover

minirust. A precise specification for "Rust lite / MIR plus"

rustc_public. Define compiler intermediate representation usable by external tools

ltex-ls. LTeX Language Server: LSP language server for LanguageTool :mag::heavy_check_mark: with support for LaTeX :mortar_board:, Markdown :pencil:, and others

lang-team. Home of the Rust lang team

linol. Wrapper around the OCaml `lsp` library to make it easier to write LSP servers

high-assurance-rust. A free book about developing secure and robust systems software.

rfcs. RFCs for changes to Rust

infer. A static analyzer for Java, C, C++, and Objective-C

z. z - jump around

object. A unified interface for reading and writing object file formats

egg. egg is a flexible, high-performance e-graph library

Kind. A modern proof language

CreuSAT. CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

kani. Kani Rust Verifier

whycode. OCaml

alt-ergo. OCamlPro public development repository for Alt-Ergo

wg.

wg-async. Working group dedicated to improving the foundations of Async I/O in Rust

platform. Multi platform setup for Rocq, Rocq libraries and tools

momo. A Rust proc_macro_attribute to outline conversions from generic functions

ballerina-lang. The Ballerina Programming Language

cameleer. A Deductive Verification Tool for OCaml Programs

pest. The Elegant Parser

miri. An interpreter for Rust's mid-level intermediate representation

gccrs. GCC Front-End for Rust

Odin. Odin Programming Language

elle. Black-box transactional safety checker based on cycle detection

gobra. Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

nomicon. The Dark Arts of Advanced and Unsafe Rust Programming

cqfd. A why3 certified prover for propositional logic

bgp-battleships. Play battleships using BGP

zz. 🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C

rosc. An OSC library for Rust.

probe-run. Run embedded programs just like native ones

atsamd. Target atsamd microcontrollers using Rust

enso. Enso Analytics is a self-service data prep and analysis platform designed for data teams.

OpenTTD. OpenTTD is an open source simulation game based upon Transport Tycoon Deluxe

prusti-dev. A static verifier for Rust, based on the Viper verification infrastructure.

cargo-expand. Subcommand to show result of macro expansion

byteorder. Rust library for reading/writing numbers in big-endian and little-endian.

compiler-explorer. Run compilers interactively from your web browser and interact with the assembly

bitvec. A crate for managing memory bit by bit

hacspec. Please see https://github.com/hacspec/hax

cargo-embed. a cargo extension for working with microcontrollers

probe-rs. A debugging toolset and library for debugging embedded ARM and RISC-V targets on a separate host

itertools. Extra iterator adaptors, iterator methods, free functions, and macros.

ghc-whole-program-compiler-project. GHC Whole Program Compiler and External STG IR tooling

rtic. Real-Time Interrupt-driven Concurrency (RTIC) framework for ARM Cortex-M microcontrollers

sqlx. 🧰 The Rust SQL Toolkit. An async, pure Rust SQL crate featuring compile-time checked queries without a DSL. Supports PostgreSQL, MySQL, and SQLite.

julia. The Julia Programming Language

cdf-program-logics. Companion Coq development for Xavier Leroy's 2021 lectures on program logics

MIRAI. Rust mid-level IR Abstract Interpreter

futhark. :boom::computer::boom: A data-parallel functional programming language

FStar. A Proof-oriented Programming Language

tutoriel_wp. Frama-C and WP tutorial

mold. mold: A Modern Linker 🦠

project-thir-unsafeck. Tracking the project to refactor the unsafe check to operate on THIR

cargo-flash. a cargo extension for programming microcontrollers

mcu-starter-projects. Simple starter projects for bare-metal MCU development

SAMD21-M0-Mini. Notes on using the Chinese "SAMD21-M0-Mini" board

berty. Berty is a secure peer-to-peer messaging app that works with or without internet access, cellular data or trust in the network

rpds. Rust persistent data structures

program-proofs-with-why3. Some programs from Rustan Leino's "Program Proofs", in Why3.

ocamlgraph. OCaml graph library

lang_tester. Rust testing framework for compilers and VMs

rust-prehistory. historical archive of rust pre-publication development

happy. The Happy parser generator for Haskell

proc-macro2. Rust

quickcheck. Automated property based testing for Rust (with shrinking).

v. Simple, fast, safe, compiled language for developing maintainable software. Compiles itself in <1s with zero library dependencies. Supports automatic C => V translation. https://vlang.io

cubical. An experimental library for Cubical Agda

z3.rs. Rust bindings for the Z3 solver.

Nim. Nim is a statically typed compiled systems programming language. It combines successful concepts from mature languages like Python, Ada and Modula. Its design focuses on efficiency, expressiveness, and elegance (in that order of priority).

obsidian-citation-plugin. Obsidian plugin which integrates your academic reference manager with the Obsidian editor. Search your references from within Obsidian and automatically create and reference literature notes for papers and books.

catala. Programming language for literate programming law specification

compiler-team. A home for compiler team planning documents, meeting minutes, and other such things.

metarocq. Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

gleam. ⭐️ A friendly language for building type-safe, scalable systems!