-
ImDecorr Public
Forked from Ades91/ImDecorr -
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 UpdatedAug 25, 2026 -
nixpkgs Public
Forked from NixOS/nixpkgsNix Packages collection & NixOS
Nix MIT License UpdatedAug 25, 2026 -
opam-coq-archive Public
Forked from rocq-prover/opamArchive for all Coq related OPAM packages organized in various repositories
-
ConCert Public
Forked from AU-COBRA/ConCertA framework for smart contract verification in Coq
Rocq Prover MIT License UpdatedMar 17, 2026 -
cakeml-backend Public
Forked from peregrine-project/cakeml-backendRocq Prover MIT License UpdatedMar 12, 2026 -
rocq-verified-extraction Public
Forked from MetaRocq/rocq-verified-extractionVerified Extraction from Rocq to OCaml/Malfunction
Coq MIT License UpdatedMar 12, 2026 -
metacoq Public
Forked from MetaRocq/metarocqMetaprogramming in Coq
Rocq Prover MIT License UpdatedMar 11, 2026 -
CompCert Public
Forked from AbsInt/CompCertThe CompCert formally-verified C compiler
Rocq Prover Other UpdatedMar 5, 2026 -
certicoq Public
Forked from CertiRocq/certirocqA Verified Compiler for Gallina, Written in Gallina
Rocq Prover MIT License UpdatedMar 5, 2026 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Rocq Prover Other UpdatedMar 4, 2026 -
agda2lambox Public
Forked from agda/agda2lamboxCompiling Agda's internal syntax to λ-box terms.
Haskell Other UpdatedFeb 17, 2026 -
lambda-box-extraction Public
Forked from peregrine-project/peregrine-toolRocq Prover MIT License UpdatedFeb 10, 2026 -
-
rocq-imp Public
Forked from peregrine-project/rocq-impToy application of Peregrine tool
Rocq Prover MIT License UpdatedJan 28, 2026 -
OVN Public
Forked from AU-COBRA/OVNVerified implementation of the Open Vote Network protocol
Rocq Prover MIT License UpdatedJan 25, 2026 -
coq-primitive Public
Forked from peregrine-project/rocq-primitiveOCaml GNU Lesser General Public License v2.1 UpdatedJan 23, 2026 -
-
jscoq Public
Forked from jscoq/jscoqA port of Coq to Javascript -- Run Coq in your Browser
TypeScript Other UpdatedNov 22, 2025 -
ssprove Public
Forked from SSProve/ssproveA foundational framework for modular cryptographic proofs in Coq
Rocq Prover MIT License UpdatedNov 12, 2025 -
jscoq-addons Public
Forked from jscoq/addonsA workspace for jsCoq addons
Makefile UpdatedNov 6, 2025 -
coq-serapi Public
Forked from rocq-archive/coq-serapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
Coq Other UpdatedOct 22, 2025 -
au-fsv Public
Docker container for Formal Software Verification course
-
hax Public
Forked from cryspen/haxA Rust verification tool
OCaml Apache License 2.0 UpdatedJul 3, 2025 -
rocq-prover.org Public
Forked from rocq-prover/rocq-prover.orgThe Rocq Prover Website
HTML Other UpdatedJun 11, 2025 -
coq-rust-extraction Public
Forked from AU-COBRA/coq-rust-extractionCoq plugin for extracting Rust code
Rocq Prover MIT License UpdatedJun 11, 2025 -
coq-elm-extraction Public
Forked from AU-COBRA/coq-elm-extractionCoq plugin for extracting Elm code
Rocq Prover MIT License UpdatedJun 11, 2025 -
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Rocq Prover Other UpdatedJun 11, 2025 -
coq 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…
OCaml GNU Lesser General Public License v2.1 UpdatedJun 11, 2025 -
math-comp Public
Forked from math-comp/math-compMathematical Components
Coq Other UpdatedJun 6, 2025
{{ message }}