Explore projects

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

Separation Logic with Characteristic Formulae Entirely within Coq

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

Itauto: an Extensible Intuitionistic SAT Solver

Itauto: an Extensible Intuitionistic SAT Solver

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

Fork of https://github.com/smtcoq/smtcoq.

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

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.

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

Coq formalization of Tes.