-
-
ImDecorr Public
Forked from Ades91/ImDecorr -
agda2lambox Public
Forked from agda/agda2lamboxCompiling Agda's internal syntax to λ-box terms.
Haskell Other UpdatedNov 26, 2025 -
certicoq Public
Forked from CertiCoq/certicoqA Verified Compiler for Gallina, Written in Gallina
Rocq Prover MIT License UpdatedNov 26, 2025 -
jscoq Public
Forked from jscoq/jscoqA port of Coq to Javascript -- Run Coq in your Browser
TypeScript Other UpdatedNov 22, 2025 -
rocq-verified-extraction Public
Forked from MetaRocq/rocq-verified-extractionVerified Extraction from Rocq to OCaml/Malfunction
Coq MIT License UpdatedNov 20, 2025 -
coq-primitive Public
Forked from palmskog/coq-primitiveOCaml GNU Lesser General Public License v2.1 UpdatedNov 20, 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 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Rocq Prover Other 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
-
OVN Public
Forked from AU-COBRA/OVNVerified implementation of the Open Vote Network protocol
Rocq Prover MIT License UpdatedJul 9, 2025 -
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 -
lambda-box-extraction Public
Forked from peregrine-project/lambda-box-extractionRocq Prover MIT License UpdatedJun 11, 2025 -
metacoq Public
Forked from MetaRocq/metarocqMetaprogramming in Coq
Rocq Prover MIT License UpdatedJun 11, 2025 -
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Rocq Prover Other UpdatedJun 11, 2025 -
nixpkgs Public
Forked from NixOS/nixpkgsNix Packages collection & NixOS
Nix MIT License UpdatedJun 11, 2025 -
ConCert Public
Forked from AU-COBRA/ConCertA framework for smart contract verification in Coq
Rocq Prover MIT License 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 -
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 UpdatedJun 11, 2025 -
opam-coq-archive Public
Forked from rocq-prover/opamArchive for all Coq related OPAM packages organized in various repositories
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 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedApr 3, 2025 -
base Public
Forked from janestreet/baseStandard library for OCaml
OCaml MIT License UpdatedApr 3, 2025 -
-
coq-lsp Public
Forked from ejgallego/rocq-lspLanguage Server Protocol for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedJan 8, 2025
{{ message }}