rocq 开源项目推荐（106 个）

formal-land /rocq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

UniMath /UniMath

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

math-comp /math-comp

数学组成部分

MetaRocq /metarocq

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

rocq-prover /vsrocq

Visual Studio Code for Coq 扩展

stepchowfun /proofs

My personal repository of formally verified mathematics.

formal-land /rocq-of-ocaml

Formal verification for OCaml, with Rocq

mit-pdos /perennial

Verifying concurrent storage and distributed systems

lukaszcz /coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

math-comp /analysis

Mathematical Components compliant Analysis Library

rocq-prover /equations

A function definition package for Rocq

uhub /awesome-coq

A curated list of awesome Coq frameworks, libraries and software.

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.

rocq-community /rocq-lsp

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]

theorem-labs /oss-verify-proofs

Theorem statements about OSS-Fuzz fuzz targets as compiled RISC-V binaries, and machine-checked Rocq proofs of them

bloomberg /crane

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

theorem-labs /oss-verify

OSS Verify: enrollment and build instructions for formally verifying open-source fuzz targets

typetheoryforall /FVjobs

A Job Board for Formal Verification

theorem-labs /rocq-linux-process-semantics

A Rocq model of a Linux process that runs a RISC-V binary

formal-land /rocq-of-solidity

Formal verification for Solidity smart contracts with the theorem prover Rocq. Providing higher security in a time of smarter AIs.