GitHub topics: rocq
rocq-prover/vsrocq
Visual Studio Code extension for Coq
Language: OCaml - Size: 78.8 MB - Last synced at: 1 day ago - Pushed at: 3 days ago - Stars: 386 - Forks: 81

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: 1.98 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 153 - Forks: 16

UniMath/UniMath
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Language: Coq - Size: 61.6 MB - Last synced at: 2 days ago - Pushed at: 21 days ago - Stars: 985 - Forks: 176

ejgallego/coq-lsp
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq
Language: OCaml - Size: 29.6 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 169 - Forks: 43

MetaRocq/metarocq
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Language: Coq - Size: 33.2 MB - Last synced at: 5 days ago - Pushed at: 7 days ago - Stars: 445 - Forks: 89

TheoWinterhalter/local-comp
WIP Local computation rules in type theory
Language: Coq - Size: 305 KB - Last synced at: 8 days ago - Pushed at: 9 days ago - Stars: 1 - Forks: 0

JetBrains-Research/big-rocq
BigRocq is a utility, that takes a Rocq (former Coq) project as input and uses domain knowladge to increase a number of theorems in the dataset by a significant factor.
Language: TypeScript - Size: 112 MB - Last synced at: 10 days ago - Pushed at: 11 days ago - Stars: 1 - Forks: 0

LLM4Rocq/miniF2F-rocq
A Rocq version of the miniF2F dataset
Language: Coq - Size: 370 KB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 18 - Forks: 0

shauryashaurya/elegant
Proof checker from scratch in Python and coq / rocq
Language: Jupyter Notebook - Size: 38.5 MB - Last synced at: 7 days ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0
