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
verifast
Research prototype tool for modular formal verification of C and Java programs
Rust325other
3 months ago
Kalman-and-Bayesian-Filters-in-Python
Kalman Filter book using Jupyter Notebook. Focuses on building intuition and exp
Jupyter Notebook15138other
5 months ago
infotheo
A Coq formalization of information theory and linear error-correcting codes
Coq60lgpl-2.1
6 months ago
convexityerror-correcting-codesinformation-theory
verdi
A framework for formally verifying distributed systems implementations in Coq
Coq559bsd-2-clause
6 months ago
coqcoq-librarydistributed-systems
GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
Coq160lgpl-3.0
6 months ago
archimedescontinuitycoq
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
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
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
tarjan
Formalization of Tarjan 72 algorithm in Coq with mathematical components and ssr
Coq9
last year
coqmathcompssreflect
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