Lean 4 programming language and theorem prover

FunTAL: mixing a functional language with assembly.

Modular And Compositional analysis with KLEE Engine

Verification working group

Constant-Time Toolkit

American Fuzzy Lop + Dyninst == AFL Fuzzing blackbox binaries

A cheatsheet of modern C++ language and library features.

Verified Assembly Language for Everest

A Clash playground/starter kit, using Nix

Comprehensive timing leak protection for Rust programs https://www.chosenplaintext.ca/open-source/rust-timing-shield/

Tink is a multi-language, cross-platform, open source library that provides cryptographic APIs that are secure, easy to use correctly, and hard(er) to misuse.

BLAKE2 official implementations

Coq to Rust program extraction. The whole tree is on the original Coq code base.

Go server for two-man rule style file encryption and decryption.

Resources for the online Type Theory Study Group

Repository for the Stacks Project

The Z3 Theorem Prover

The Mechanization of Standard ML

Type-driven code generation for OCaml

Servo aims to empower developers with a lightweight, high-performance alternative for embedding web technologies in applications.

property-based testing for C: generate input to find obscure bugs, then reduce to minimal failing input

A demo implementation of a simple dependently-typed language

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

Empowering everyone to build reliable and efficient software.

Haskell LLVM JIT Compiler Tutorial

πfs - the data-free filesystem!