infotheo
A Coq formalization of information theory and linear error-correcting codes
Coq60lgpl-2.1
6 months ago
convexityerror-correcting-codesinformation-theory
RecordFlux
Formal specification and generation of verifiable binary parsers, message genera
Ada95agpl-3.0
6 months ago
adabinary-parsercommunication-protocol
fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Coq135other
7 months ago
coqcoq-cifour-color-theorem
coq
Coq is a formal proof management system. It provides a formal language to write
OCaml4576lgpl-2.1
2 months ago
coqdependent-typesproof-assistant
GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
Coq160lgpl-3.0
6 months ago
archimedescontinuitycoq
verifast
Research prototype tool for modular formal verification of C and Java programs
Rust325other
3 months ago
tarjan
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly
Coq11
9 months ago
coqmathcompmathcomp-ci
category-theory
An axiom-free formalization of category theory in Coq for personal study and pra
Coq716bsd-3-clause
6 months ago
cartesiancartesian-closed-categorycategories
Kalman-and-Bayesian-Filters-in-Python
Kalman Filter book using Jupyter Notebook. Focuses on building intuition and exp
Jupyter Notebook15138other
5 months ago
verdi
A framework for formally verifying distributed systems implementations in Coq
Coq559bsd-2-clause
6 months ago
coqcoq-librarydistributed-systems
coq-haskell
A library for formalizing Haskell types and functions in Coq
Coq161bsd-3-clause
7 months ago
UniMath
This coq library aims to formalize a substantial body of mathematics using the u
Coq876other
6 months ago
coqcoq-libraryfoundations
RecordFlux
Formal specification and generation of verifiable binary parsers, message genera
Ada91agpl-3.0
last year
adabinary-parsercommunication-protocol
tarjan
Formalization of Tarjan 72 algorithm in Coq with mathematical components and ssr
Coq9
last year
coqmathcompssreflect
SLAyer
SLAyer is an automatic formal verification tool that uses separation logic to ve
OCaml321other
8 years ago
SXML
Formally verified, bounded-stack XML library
Ada19agpl-3.0
4 years ago
adaformal-methodsformal-verification
CuBit
General-purpose, formally-verified, 64-bit operating system in SPARK/Ada for x86
Ada75gpl-3.0
3 years ago
adaosspark
iTerm-Seti_UX
A simple and minimal iTerm2 color scheme Formally known as RainCoat
JavaScript2
8 years ago
idris-ct
formally verified category theory library
Idris248agpl-3.0
4 years ago
category-theoryformal-proofsformal-verification
cdec
Decoder, aligner, and model optimizer for statistical machine translation and ot
C++184apache-2.0
4 years ago
spark-by-example
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programmi
Ada145
2 years ago
adaformal-methodsformal-specification