Topic: "coq"
rocq-prover/rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
Language: OCaml - Size: 201 MB - Last synced at: 3 days ago - Pushed at: 6 days ago - Stars: 5,317 - Forks: 707
AbsInt/CompCert
The CompCert formally-verified C compiler
Language: Rocq Prover - Size: 20.4 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 2,026 - Forks: 240
formal-land/rocq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs to make safe applications for demanding domains.
Language: Rocq Prover - Size: 135 MB - Last synced at: 6 days ago - Pushed at: 9 days ago - Stars: 1,032 - Forks: 38
UniMath/UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Language: Rocq Prover - Size: 38.1 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 992 - Forks: 186
Coq-zh/SF-zh
《软件基础》中译版 Software Foundations Chinese Translation
Language: HTML - Size: 905 MB - Last synced at: 7 months ago - Pushed at: almost 4 years ago - Stars: 940 - Forks: 69
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Language: Coq - Size: 38.5 MB - Last synced at: 3 months ago - Pushed at: almost 2 years ago - Stars: 830 - Forks: 14
jwiegley/category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Language: Rocq Prover - Size: 3.27 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 787 - Forks: 80
uwdb/Cosette
Cosette is an automated SQL solver.
Language: Lean - Size: 5.56 MB - Last synced at: 7 months ago - Pushed at: about 1 year ago - Stars: 677 - Forks: 56
math-comp/math-comp
Mathematical Components
Language: Rocq Prover - Size: 17.2 MB - Last synced at: 9 days ago - Pushed at: 11 days ago - Stars: 663 - Forks: 126
uwplse/verdi
A framework for formally verifying distributed systems implementations in Coq
Language: Rocq Prover - Size: 2.57 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 606 - Forks: 56
ProofGeneral/PG
This repo is the new home of Proof General
Language: Emacs Lisp - Size: 26.5 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 540 - Forks: 95
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
Size: 122 KB - Last synced at: 8 months ago - Pushed at: 11 months ago - Stars: 537 - Forks: 42
jscoq/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
Language: TypeScript - Size: 14.6 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 535 - Forks: 48
rocq-community/rocq-tricks
Tricks you wish the Coq manual told you [maintainer=@tchajed]
Language: Coq - Size: 232 KB - Last synced at: about 2 months ago - Pushed at: 7 months ago - Stars: 530 - Forks: 24
AeneasVerif/aeneas
A verification toolchain for Rust programs
Language: OCaml - Size: 11.5 MB - Last synced at: 4 days ago - Pushed at: 7 days ago - Stars: 496 - Forks: 39
MetaRocq/metarocq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Language: Rocq Prover - Size: 32.5 MB - Last synced at: 5 days ago - Pushed at: 18 days ago - Stars: 495 - Forks: 96
PrincetonUniversity/VST
Verified Software Toolchain
Language: Rocq Prover - Size: 76.5 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 476 - Forks: 96
rocq-prover/vsrocq
Visual Studio Code extension for Coq
Language: OCaml - Size: 79 MB - Last synced at: 5 days ago - Pushed at: 28 days ago - Stars: 427 - Forks: 91
rocq-community/awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
Size: 205 KB - Last synced at: 8 days ago - Pushed at: 2 months ago - Stars: 373 - Forks: 25
EgbertRijke/HoTT-Intro 📦
An introductory course to Homotopy Type Theory
Language: Agda - Size: 7.11 MB - Last synced at: 9 months ago - Pushed at: over 5 years ago - Stars: 365 - Forks: 28
cpitclaudel/company-coq
A Coq IDE build on top of Proof General's Coq mode
Language: Emacs Lisp - Size: 23 MB - Last synced at: 4 months ago - Pushed at: 5 months ago - Stars: 358 - Forks: 29
jasmin-lang/jasmin
Language for high-assurance and high-speed cryptography
Language: Rocq Prover - Size: 22.6 MB - Last synced at: 22 days ago - Pushed at: 22 days ago - Stars: 319 - Forks: 66
stepchowfun/proofs
My personal repository of formally verified mathematics.
Language: Rocq Prover - Size: 1.59 MB - Last synced at: 19 days ago - Pushed at: 22 days ago - Stars: 308 - Forks: 14
whonore/Coqtail
Interactive Coq Proofs in Vim
Language: Python - Size: 942 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 306 - Forks: 37
namin/llm-verified-with-monte-carlo-tree-search
LLM verified with Monte Carlo Tree Search
Language: Jupyter Notebook - Size: 42.4 MB - Last synced at: 3 months ago - Pushed at: 9 months ago - Stars: 281 - Forks: 30
QuickChick/QuickChick
Randomized Property-Based Testing Plugin for Coq
Language: Rocq Prover - Size: 27.7 MB - Last synced at: 17 days ago - Pushed at: 20 days ago - Stars: 278 - Forks: 50
formal-land/coq-of-ocaml
Formal verification for OCaml
Language: OCaml - Size: 17.6 MB - Last synced at: 8 months ago - Pushed at: over 1 year ago - Stars: 263 - Forks: 20
mattam82/Coq-Equations
A function definition package for Coq
Language: Coq - Size: 59.5 MB - Last synced at: 16 days ago - Pushed at: 18 days ago - Stars: 234 - Forks: 53
math-comp/analysis
Mathematical Components compliant Analysis Library
Language: Rocq Prover - Size: 52.8 MB - Last synced at: 1 day ago - Pushed at: 3 days ago - Stars: 231 - Forks: 64
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
Language: OCaml - Size: 2.56 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 231 - Forks: 34
LogicalAtomist/principia-rewrite
The Principia Rewrite
Language: TeX - Size: 12.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 229 - Forks: 6
rocq-community/fourcolor
Formal proof of the Four Color Theorem [maintainer=@ybertot]
Language: Rocq Prover - Size: 803 KB - Last synced at: 5 days ago - Pushed at: 3 months ago - Stars: 224 - Forks: 23
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
Size: 25.4 KB - Last synced at: 3 days ago - Pushed at: about 4 years ago - Stars: 216 - Forks: 10
GeoCoq/GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
Language: Rocq Prover - Size: 7.74 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 200 - Forks: 28
ejgallego/rocq-lsp
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq
Language: OCaml - Size: 31.5 MB - Last synced at: 5 days ago - Pushed at: about 1 month ago - Stars: 195 - Forks: 51
IBM/ACE-RISCV
Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.
Language: Rust - Size: 2.08 MB - Last synced at: 27 days ago - Pushed at: 28 days ago - Stars: 194 - Forks: 19
uwplse/verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Language: Coq - Size: 2.96 MB - Last synced at: 9 months ago - Pushed at: about 2 years ago - Stars: 186 - Forks: 19
LPCIC/coq-elpi
Coq plugin embedding elpi
Language: Rocq Prover - Size: 12 MB - Last synced at: 16 days ago - Pushed at: 18 days ago - Stars: 177 - Forks: 69
rocq-community/math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
Language: Rocq Prover - Size: 2.88 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 167 - Forks: 43
ilyasergey/pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Language: Coq - Size: 6.47 MB - Last synced at: 8 months ago - Pushed at: over 4 years ago - Stars: 164 - Forks: 19
namin/dot
formalization of the Dependent Object Types (DOT) calculus
Size: 4.57 MB - Last synced at: 3 months ago - Pushed at: over 9 years ago - Stars: 161 - Forks: 12
mit-plv/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Language: Rocq Prover - Size: 4.2 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 160 - Forks: 30
rocq-prover/opam
Archive for all Rocq and Coq-related opam packages organized in various repositories
Language: OCaml - Size: 12.7 MB - Last synced at: 6 days ago - Pushed at: 9 days ago - Stars: 157 - Forks: 177
CertiCoq/certicoq
A Verified Compiler for Gallina, Written in Gallina
Language: Rocq Prover - Size: 32.4 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 156 - Forks: 32
mit-plv/koika
A core language for rule-based hardware design 🦑
Language: Rocq Prover - Size: 4.54 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 156 - Forks: 14
discus-lang/iron
Coq formalizations of functional languages.
Language: Coq - Size: 800 KB - Last synced at: 9 months ago - Pushed at: over 5 years ago - Stars: 143 - Forks: 8
rocq-community/coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Language: Rocq Prover - Size: 3.1 MB - Last synced at: 5 days ago - Pushed at: 3 months ago - Stars: 137 - Forks: 52
goose-lang/goose
Goose converts a subset of Go to Rocq
Language: Go - Size: 4.14 MB - Last synced at: 3 days ago - Pushed at: 6 days ago - Stars: 135 - Forks: 18
rocq-archive/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Language: Coq - Size: 5.8 MB - Last synced at: 3 months ago - Pushed at: 4 months ago - Stars: 133 - Forks: 40
rocq-community/coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Language: Coq - Size: 545 KB - Last synced at: 5 days ago - Pushed at: 11 months ago - Stars: 126 - Forks: 26
AU-COBRA/ConCert
A framework for smart contract verification in Coq
Language: Rocq Prover - Size: 14.5 MB - Last synced at: 30 days ago - Pushed at: about 1 month ago - Stars: 124 - Forks: 22
verse-lab/ceramist
Verified hash-based AMQ structures in Coq
Language: Coq - Size: 1.04 MB - Last synced at: 3 days ago - Pushed at: over 5 years ago - Stars: 124 - Forks: 5
project-oak/silveroak 📦
Formal specification and verification of hardware, especially for security and privacy.
Language: Coq - Size: 36.1 MB - Last synced at: 12 months ago - Pushed at: over 3 years ago - Stars: 123 - Forks: 20
uds-psl/coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Language: Coq - Size: 13.7 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 120 - Forks: 31
ilya-klyuchnikov/ttlite
A SuperCompiler for Martin-Löf's Type Theory
Language: Scala - Size: 1.5 MB - Last synced at: 9 months ago - Pushed at: almost 4 years ago - Stars: 120 - Forks: 9
rocq-community/corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
Language: Rocq Prover - Size: 10.9 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 115 - Forks: 46
WasmCert/WasmCert-Coq
A mechanisation of Wasm in Coq(Rocq)
Language: Rocq Prover - Size: 4.71 MB - Last synced at: 3 days ago - Pushed at: 19 days ago - Stars: 112 - Forks: 15
verse-lab/toychain
A minimalistic blockchain consensus implemented and verified in Coq
Language: Coq - Size: 635 KB - Last synced at: 7 months ago - Pushed at: over 5 years ago - Stars: 112 - Forks: 12
JetBrains-Research/coqpilot
VSCode extension that is designed to help automate writing of Coq proofs.
Language: TypeScript - Size: 19 MB - Last synced at: 6 months ago - Pushed at: 7 months ago - Stars: 109 - Forks: 4
math-comp/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
Language: Rocq Prover - Size: 10.6 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 103 - Forks: 25
DistributedComponents/disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Language: Coq - Size: 1.24 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 100 - Forks: 7
sec-bit/tokenlibs-with-proofs
Correctness proofs of Ethereum token contracts
Language: Coq - Size: 268 KB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 98 - Forks: 23
rocq-community/coq-dpdgraph
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
Language: Rocq Prover - Size: 387 KB - Last synced at: 5 days ago - Pushed at: 17 days ago - Stars: 97 - Forks: 33
ymherklotz/vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Language: Rocq Prover - Size: 21.9 MB - Last synced at: 11 days ago - Pushed at: 13 days ago - Stars: 96 - Forks: 6
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
Language: Coq - Size: 596 KB - Last synced at: 8 months ago - Pushed at: about 1 year ago - Stars: 96 - Forks: 4
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
Language: Python - Size: 414 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 95 - Forks: 8
siegebell/vscoq
Coq Support for Visual Studio Code
Language: TypeScript - Size: 1.52 MB - Last synced at: 2 months ago - Pushed at: about 6 years ago - Stars: 92 - Forks: 9
inQWIRE/SQIR
A Small Quantum Intermediate Representation
Language: Rocq Prover - Size: 29.3 MB - Last synced at: 4 months ago - Pushed at: 5 months ago - Stars: 87 - Forks: 24
SkyLabsAI/BRiCk
Formalization of C++ for verification purposes.
Language: Rocq Prover - Size: 114 MB - Last synced at: 17 days ago - Pushed at: 18 days ago - Stars: 85 - Forks: 15
plclub/hs-to-coq
Convert Haskell source code to Coq source code.
Language: Coq - Size: 10.5 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 85 - Forks: 9
jaalonso/Lecturas_GLC
Readings on computational logic, interactive theorem proving and functional programming.
Size: 3.25 MB - Last synced at: 4 days ago - Pushed at: 8 days ago - Stars: 84 - Forks: 8
alhassy/next-700-module-systems
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
Language: HTML - Size: 80.9 MB - Last synced at: 2 months ago - Pushed at: about 4 years ago - Stars: 82 - Forks: 6
coq-tactician/coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
Language: OCaml - Size: 2.23 MB - Last synced at: 16 days ago - Pushed at: 19 days ago - Stars: 79 - Forks: 24
JBakouny/Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Language: Scala - Size: 17.6 MB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 79 - Forks: 7
sifive/RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Language: Haskell - Size: 26.8 MB - Last synced at: 2 months ago - Pushed at: over 5 years ago - Stars: 78 - Forks: 7
imdea-software/htt
Hoare Type Theory
Language: Rocq Prover - Size: 560 KB - Last synced at: 6 months ago - Pushed at: 7 months ago - Stars: 76 - Forks: 6
rocq-community/hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Language: Coq - Size: 20.9 MB - Last synced at: 8 months ago - Pushed at: 12 months ago - Stars: 75 - Forks: 12
ml4tp/gamepad
A Learning Environment for Theorem Proving
Language: Coq - Size: 53.8 MB - Last synced at: 9 months ago - Pushed at: over 3 years ago - Stars: 73 - Forks: 15
rocq-community/coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Language: Rocq Prover - Size: 2.06 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 72 - Forks: 17
rocq-community/manifesto
Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.
Size: 213 KB - Last synced at: 3 days ago - Pushed at: 9 months ago - Stars: 68 - Forks: 6
mit-plv/rupicola
Gallina to Bedrock2 compilation toolkit
Language: Rocq Prover - Size: 1.65 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 64 - Forks: 14
rocq-community/coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
Language: HTML - Size: 353 KB - Last synced at: 3 days ago - Pushed at: about 1 month ago - Stars: 61 - Forks: 15
rocq-community/autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Language: Coq - Size: 913 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 59 - Forks: 15
choukh/Set-Theory
A formalization of the textbook Elements of Set Theory
Language: Coq - Size: 3.79 MB - Last synced at: 6 months ago - Pushed at: over 4 years ago - Stars: 59 - Forks: 4
rocq-community/semantics
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
Language: Rocq Prover - Size: 130 KB - Last synced at: 5 days ago - Pushed at: about 1 month ago - Stars: 57 - Forks: 4
anton-trunov/csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
Language: HTML - Size: 3.75 MB - Last synced at: 2 months ago - Pushed at: almost 3 years ago - Stars: 57 - Forks: 14
sigurdschneider/lvc
LVC verified compiler
Language: Coq - Size: 5.64 MB - Last synced at: 9 months ago - Pushed at: about 7 years ago - Stars: 57 - Forks: 2
SatyendraBanjare/plt-formal-methods-resources
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
Size: 3.24 MB - Last synced at: 9 months ago - Pushed at: over 6 years ago - Stars: 55 - Forks: 1
philzook58/nand2coq
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
Language: Coq - Size: 823 KB - Last synced at: 9 months ago - Pushed at: about 4 years ago - Stars: 54 - Forks: 3
lthms/FreeSpec
A framework for implementing and certifying impure computations in Coq
Language: Coq - Size: 958 KB - Last synced at: 2 months ago - Pushed at: almost 2 years ago - Stars: 53 - Forks: 11
ejgallego/pycoq
Python bindings for the Coq interactive proof assistant
Language: OCaml - Size: 39.1 KB - Last synced at: 9 months ago - Pushed at: almost 4 years ago - Stars: 53 - Forks: 4
tchajed/iris-simp-lang
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
Language: Rocq Prover - Size: 1.31 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 51 - Forks: 5
rocq-community/topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Language: Coq - Size: 770 KB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 51 - Forks: 11
uwplse/PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Language: OCaml - Size: 1.73 MB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 51 - Forks: 2
andrew-bedford/coqatoo
Generates natural language versions of Coq proofs
Language: Java - Size: 7.55 MB - Last synced at: 9 months ago - Pushed at: almost 8 years ago - Stars: 51 - Forks: 1
math-comp/finmap
Finite sets, finite maps, multisets and generic sets
Language: Rocq Prover - Size: 737 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 50 - Forks: 29
rocq-community/fav-ssr
Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]
Language: Rocq Prover - Size: 354 KB - Last synced at: 3 days ago - Pushed at: 3 months ago - Stars: 50 - Forks: 7
uwplse/pumpkin-pi
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Language: Coq - Size: 3.45 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 49 - Forks: 9
rocq-community/coq-nix-toolbox
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
Language: Nix - Size: 1.09 MB - Last synced at: 3 days ago - Pushed at: 28 days ago - Stars: 48 - Forks: 21
rocq-community/reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Language: Coq - Size: 552 KB - Last synced at: 5 days ago - Pushed at: 9 months ago - Stars: 47 - Forks: 7