-
CompCert Public
Forked from AbsInt/CompCertThe CompCert formally-verified C compiler
Coq Other UpdatedJun 26, 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 10, 2025 -
bedrock2 Public
Forked from mit-plv/bedrock2A work-in-progress language and compiler for verified low-level programming
Coq MIT License UpdatedMay 21, 2025 -
corn Public
Forked from rocq-community/cornCoq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
Coq GNU General Public License v2.0 UpdatedMay 21, 2025 -
VST Public
Forked from PrincetonUniversity/VSTVerified Software Toolchain
Coq Other UpdatedMay 21, 2025 -
coq-dpdgraph Public
Forked from rocq-community/coq-dpdgraphBuild dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
Coq GNU Lesser General Public License v2.1 UpdatedMay 21, 2025 -
metarocq Public
Forked from MetaRocq/metarocqMetaprogramming, verified meta-theory and implementation of Rocq in Rocq
Coq MIT License UpdatedMay 21, 2025 -
stdlib Public
Forked from rocq-prover/stdlibStdlib for the Rocq Prover
Coq GNU Lesser General Public License v2.1 UpdatedMay 19, 2025 -
argosy Public
Forked from mit-pdos/argosyProving crash safety for systems with layered recovery
Coq MIT License UpdatedMay 13, 2025 -
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 UpdatedMay 13, 2025 -
weierstrass Public
Forked from damien-pous/weierstrassWeierstrass' theorem in Rocq
Coq GNU General Public License v3.0 UpdatedFeb 20, 2025 -
-
llvm-project Public
Forked from llvm/llvm-projectThe LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at…
UpdatedAug 19, 2022 -
-
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 UpdatedNov 8, 2021 -
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
OCaml GNU Lesser General Public License v2.1 UpdatedJul 28, 2021 -
-
codegen Public
Forked from akr/codegenCoq plugin for monomorphization and C code generation
OCaml GNU Lesser General Public License v2.1 UpdatedJun 9, 2021 -
opam-repository Public
Forked from ocaml/opam-repositoryMain public package repository for OPAM, the source package manager of OCaml.
-
fiat-crypto Public
Forked from mit-plv/fiat-cryptoCryptographic Primitive Code Generation by Fiat
Coq MIT License UpdatedApr 9, 2021 -
coqprime Public
Forked from thery/coqprimePrime numbers for Coq
Coq GNU Lesser General Public License v2.1 UpdatedApr 9, 2021 -
bignums Public
Forked from rocq-community/bignumsCoq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Coq GNU Lesser General Public License v2.1 UpdatedApr 9, 2021 -
mythril Public
Forked from mythril-hypervisor/mythrilA hypervisor written in rust
Rust MIT License UpdatedOct 25, 2020 -
-
cross-crypto Public
Forked from mit-plv/cross-cryptoConnecting computational and symbolic crypto models
Coq MIT License UpdatedMay 13, 2020 -
fcf Public
Forked from adampetcher/fcfFoundational Cryptography Framework for machine-checked proofs of cryptography.
Coq Other UpdatedMay 11, 2020 -
kami Public
Forked from mit-plv/kamiA Platform for High-Level Parametric Hardware Specification and its Modular Verification
Coq MIT License UpdatedMay 11, 2020 -
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 UpdatedMay 11, 2020 -
-
verdi Public
Forked from uwplse/verdiA framework for formally verifying distributed systems implementations in Coq
Coq BSD 2-Clause "Simplified" License UpdatedJan 31, 2020