Systems language with linear types and capability-based security.

The HOL Light theorem prover

The Ott tool for writing definitions of programming languages and calculi

Proof assistant based on the λΠ-calculus modulo rewriting

A proof assistant for higher-dimensional type theory

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

CN separation logic refinement type system for C

Experimental model checker for testing concurrent algorithms

An automated deductive program verifier based on concurrent separation logic

Topochecker, a topological model checker

The Cubicle model checker

Mostly Automated Proof Repair for Verified Libraries