-
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Coq Other UpdatedJan 16, 2026 -
mathcomp Public
Forked from math-comp/math-compMathematical Components
Rocq Prover Other UpdatedJan 16, 2026 -
nixpkgs Public
Forked from NixOS/nixpkgsNix Packages collection & NixOS
Nix MIT License UpdatedJan 16, 2026 -
bigenough Public
Forked from math-comp/bigenoughAsymptotic reasoning with bigenough
Coq UpdatedJan 13, 2026 -
stdlib Public
Forked from rocq-prover/stdlibStdlib for the Rocq Prover
Coq GNU Lesser General Public License v2.1 UpdatedJan 13, 2026 -
-
coq-nix-toolbox Public
Forked from rocq-community/coq-nix-toolboxNix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
Nix MIT License UpdatedJan 13, 2026 -
perennial Public
Forked from mit-pdos/perennialVerifying concurrent crash-safe systems
Coq MIT License UpdatedJan 10, 2026 -
-
rocq Public
Forked from rocq-prover/rocqCoq 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 develo…
-
fiat-crypto Public
Forked from mit-plv/fiat-cryptoCryptographic Primitive Code Generation by Fiat
Coq Other UpdatedJan 10, 2026 -
-
cross-crypto Public
Forked from mit-plv/cross-cryptoConnecting computational and symbolic crypto models
Coq MIT License UpdatedJan 10, 2026 -
bedrock2 Public
Forked from mit-plv/bedrock2A work-in-progress language and compiler for verified low-level programming
Coq MIT License UpdatedJan 10, 2026 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedJan 9, 2026 -
fiat Public
Forked from mit-plv/fiatMostly Automated Synthesis of Correct-by-Construction Programs
Coq Other UpdatedJan 9, 2026 -
VST Public
Forked from PrincetonUniversity/VSTVerified Software Toolchain
Coq Other UpdatedJan 9, 2026 -
category-theory Public
Forked from jwiegley/category-theoryAn axiom-free formalization of category theory in Coq for personal study and practical work
Coq BSD 3-Clause "New" or "Revised" License UpdatedJan 9, 2026 -
color Public
Forked from fblanqui/colorCoq library on rewriting theory and termination
Coq Other UpdatedJan 9, 2026 -
rewriter Public
Forked from mit-plv/rewriterReflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq Other UpdatedJan 9, 2026 -
fcf Public
Forked from adampetcher/fcfFoundational Cryptography Framework for machine-checked proofs of cryptography.
Coq Other UpdatedJan 9, 2026 -
verdi-raft Public
Forked from uwplse/verdi-raftAn implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Coq BSD 2-Clause "Simplified" License UpdatedJan 9, 2026 -
coqhammer Public
Forked from lukaszcz/coqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
OCaml Other UpdatedJan 9, 2026 -
-
verdi Public
Forked from uwplse/verdiA framework for formally verifying distributed systems implementations in Coq
Rocq Prover BSD 2-Clause "Simplified" License UpdatedJan 9, 2026 -
-
StructTact Public
Forked from uwplse/StructTactCoq utility and tactic library.
Coq BSD 2-Clause "Simplified" License UpdatedJan 9, 2026 -
coq-ceres Public
Forked from Lysxia/coq-ceresCoq library for serialization to S-expressions
Coq MIT License UpdatedJan 9, 2026 -
kami Public
Forked from mit-plv/kamiA Platform for High-Level Parametric Hardware Specification and its Modular Verification
Coq MIT License UpdatedJan 8, 2026 -
riscv-coq Public
Forked from mit-plv/riscv-coqRISC-V Specification in Coq
Coq BSD 3-Clause "New" or "Revised" License UpdatedJan 8, 2026
{{ message }}