Explore projects

SHENGHAO Yuan / CertrBPFJIT
GNU General Public License v2.0 or laterUpdated 
Updated

Why3 / why3
GNU Lesser General Public License v2.1 onlyWhy3 is a software verification platform, featuring a versatile MLstyle language and interfaces to various powerful automated and interactive theorem provers.
Updated 



Updated

GILBERT Gaëtan / coq
GNU Lesser General Public License v2.1 onlyMirror for CI/CD purposes only.
Updated 
Flocq / flocq
OtherFlocq (Floats for Coq) is a floatingpoint formalization for the Coq system. It provides a comprehensive library of theorems on a multiradix multiprecision arithmetic. It also supports efficient numerical computations inside Coq.
Updated 
Updated

SHENGHAO Yuan / CertrBPFOpt
GNU General Public License v2.0 or laterUpdated 
Updated

GALLEGO ARIAS Emilio Jesus / itauto
MIT LicenseItauto: an Extensible Intuitionistic SAT Solver
Updated 
CoqInterval / interval
CeCILLC Free Software License AgreementCoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.
Updated 
POTTIER Francois / menhir
GNU Library General Public License v2 onlyAn LR(1) parser generator for OCaml.
Updated 
Updated

Gappa / coq
OtherA Coq tactic for discharging goals about floatingpoint arithmetic and roundoff errors using the Gappa prover.
Updated 
Coquelicot / coquelicot
OtherA Coq formalization of real analysis compatible with the standard library.
Updated 
Teaching material for an industrial audience
Updated