coq
There are 647 repositories under coq topic.
coq/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
AbsInt/CompCert
The CompCert formally-verified C compiler
UniMath/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Coq-zh/SF-zh
《软件基础》中译版 Software Foundations Chinese Translation
formal-land/coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
jwiegley/category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
uwdb/Cosette
Cosette is an automated SQL solver.
math-comp/math-comp
Mathematical Components
uwplse/verdi
A framework for formally verifying distributed systems implementations in Coq
jscoq/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
coq-community/coq-tricks
Tricks you wish the Coq manual told you [maintainer=@tchajed]
ProofGeneral/PG
This repo is the new home of Proof General
PrincetonUniversity/VST
Verified Software Toolchain
MetaCoq/metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
coq/vscoq
Visual Studio Code extension for Coq
EgbertRijke/HoTT-Intro
An introductory course to Homotopy Type Theory
cpitclaudel/company-coq
A Coq IDE build on top of Proof General's Coq mode
coq-community/awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
stepchowfun/proofs
My personal repository of formally verified mathematics.
whonore/Coqtail
Interactive Coq Proofs in Vim
jasmin-lang/jasmin
Language for high-assurance and high-speed cryptography
namin/llm-verified-with-monte-carlo-tree-search
LLM verified with Monte Carlo Tree Search
QuickChick/QuickChick
Randomized Property-Based Testing Plugin for Coq
formal-land/coq-of-ocaml
Formal verification for OCaml
AeneasVerif/aeneas
A verification toolchain for Rust programs
mattam82/Coq-Equations
A function definition package for Coq
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
math-comp/analysis
Mathematical Components compliant Analysis Library
LogicalAtomist/principia
The Principia Rewrite
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
coq-community/fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
GeoCoq/GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
uwplse/verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
mit-pdos/perennial
Verifying concurrent crash-safe systems