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

Lightweight static analysis for many languages. Find bug variants with patterns that look like source code.

Performant type-checking for python.

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

MirageOS is a library operating system that constructs unikernels

Source code of the Coccinelle project (mirror of the main Coccinelle repository located at Inria)

A verification toolchain for Rust programs

EasyCrypt: Computer-Aided Cryptographic Proofs

PDF Command Line Tools Source

OCaml library for reading, writing and modifying PDF files

The Stan transpiler (from Stan to C++ and beyond).

Lossless PDF squeezer

Generate titles of conferences in philosophy!

A tool to get TPTP problems from a TSTP proof trace

Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).