Parsing, analyzing, and comparing source code across many languages

Compiler for Elm, a functional language for reliable webapps.

A statically typed lisp, without a GC, for real-time applications.

Language, engine, and tooling for expressing, testing, and evaluating composable language rules on input strings.

A Dependently Typed Functional Programming Language

C to Rust translator

Fast, portable and reliable dependency analysis for any codebase. Supports license & vulnerability scanning for large monoliths. Language-agnostic; integrates with 20+ build systems.

A proper subset of Haskell that compiles to JavaScript

Cryptol: The Language of Cryptography

Automatic testing of Haskell programs.

Crucible is a library for symbolic simulation of imperative programs

The Oden Programming Language (NO LONGER IN ACTIVE DEVELOPMENT)

The Software Analysis Workbench

TLS/SSL implementation in haskell

Open source binary analysis tools.

An experimental grammar fuzzer in Haskell using QuickCheck

Symbolic formula representation and solver interaction library

Play Minesweeper by formally proving your moves in Idris

Program Round-off Error Certifier via Static Analysis

Test suite for implementations of Featherweight Generic Go

Compressed Bloom Filters (Golomb-compressed sequences, with indices)

Fuse-based filesystem to decode and present Sereal-encoded files