Explore projects

Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.

Separation Logic with Characteristic Formulae Entirely within Coq

An LR(1) parser generator for OCaml.

An LR(1) parser generator for OCaml.

CertrBPF: a fully verified RIOT rBPF (verifier+interpreter+JIT) in Coq

Translation validation of properties of various types of predicates at runtime, interfacing with SMTCoq for validation of SMT unsatisfiability certificates.

CoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

coqdl + verified contract theory

A Coq formalization of real analysis compatible with the standard library.

A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.

implementation and metatheory of time credits and time receipts in Iris / Coq

This repository contains the Coq/Iris proofs that accompany the paper A Separation Logic for Effect Handlers.

Coq formalization of Tes.

Abstract Interpretation with ITrees.

A Coq formalization of real analysis compatible with the standard library.