Formal Verification & Rocq Prover

21 repos

Formal verification infrastructure centered on Rocq (formerly Coq), a proof assistant for mathematically verified software. The cluster emphasizes compiler correctness and C verification through projects like CompCert, alongside tooling for proof development (LSP servers, OCaml extraction) and ecosystem support. Most repos are either Rocq prover repositories or OCaml-based tools that support formal verification workflows, making this a coherent area for learning how to write and verify provably correct code.

Rocq Prover · 16

OCaml · 2

Coq · 1

Lean · 1

Rust · 1

coq ·3,613

compiler ·2,765

compcert ·2,732

c ·2,732

formal-verification ·2,180

rust ·1,424

proof-assistant ·677

formal-specification ·579

formal-methods ·579

coq-vst ·508

Related clusters

Coq Proof Assistant and Extensions23 Rocq Proof Assistant & Type Theory18 Formal verification of cryptographic code22 VS Code Language Extensions29 Formal Mathematics in Rocq/Coq17 Cluster 43598932

mit-plv/fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

Rocq Prover

157

2,460 commits

AbsInt/CompCert

The CompCert formally-verified C compiler

Rocq Prover

2,224

2,436 commits

jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

Rocq Prover

364

4,570 commits

mit-plv/rupicola

Gallina to Bedrock2 compilation toolkit

Rocq Prover

812 commits

damien-pous/relation-algebra

Relation algebra library for Coq

Rocq Prover

184 commits

PrincetonUniversity/VST

Verified Software Toolchain

Rocq Prover

508

6,149 commits

hacspec/hacspec-v2

A Rust verification tool

Lean

474

5,203 commits

mit-plv/fiat-crypto

Cryptographic Primitive Code Generation by Fiat

Rocq Prover

839

8,337 commits

awslabs/aws-lc-verification

This repository contains specifications, proof scripts, and other artifacts required to formally…

Rocq Prover

145 commits

cryspen/hax

A Rust verification tool

OCaml

474

5,061 commits

octra-labs/amlc

amlc - applied meta lang compiler and local aml executor

OCaml

1 commits

coq/stdlib

Stdlib for the Rocq Prover

Rocq Prover

41,986 commits

rocq-prover/stdlib

Stdlib for the Rocq Prover

Rocq Prover

41,986 commits

hacspec/hax

A Rust verification tool

Rust

476

5,061 commits

mit-plv/rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and…

Rocq Prover

5,807 commits

coq-community/atbr

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

Rocq Prover

148 commits

mit-plv/kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Rocq Prover

169

598 commits

mit-plv/bedrock2

A work-in-progress language and compiler for verified low-level programming

Rocq Prover

335

3,631 commits

coq-community/coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Rocq Prover

612 commits

CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

Rocq Prover

177

2,544 commits

rocq-archive/stdlib2

No description

Coq

25 commits