An open source electric sleeping pad inflation device

Research prototype tool for modular formal verification of C and Java programs

Assembly super-optimization via constraint solving

A cube that balances itself in a corner or edge using reaction wheels

Define compiler intermediate representation usable by external tools

A DNS server that offers useful utilities and services over the DNS protocol. Weather, world time, unit conversion etc.

Shuttle is a library for testing concurrent Rust code

The glucose SAT solver

Rust task runner and build tool.

A simple, high-throughput file client for mounting an Amazon S3 bucket as a local file system.

Some programs from Rustan Leino's "Program Proofs", in Why3.

Tools to interact with why3 sessions

A verification toolchain for Rust programs

Tricks you wish the Coq manual told you

Verified Rust for low-level systems code

CCDetect-lsp VSCode plugin

Malleable Load Balancer. Massively Parallel Logic Backend. Award-winning SAT solving for the cloud.

cdsat

A computer science textbook

Three-Way Semantic Merge for Feature Model Evolution Plans

Schedule for the #PLTalk livestream. On Twitch here: https://www.twitch.tv/jeanqasaur

A superoptimizer for LLVM IR

Transcripts of Clojure-related talks

Modular Soundness Checking for Feature Model Evolution Plans

C++ `std::unique_ptr` that represents each object as an NFT on the Ethereum blockchain

Creusot helps you prove your code is correct in an automated fashion.