Cluster 633595

27 repos

Rocq Prover · 14

OCaml · 9

Coq · 2

Lean · 1

Rust · 1

coq ·5,717

compiler ·3,320

formal-verification ·2,746

c ·2,734

compcert ·2,734

rocq ·2,280

rust ·1,440

metaprogramming ·1,303

coq-formalization ·1,106

proof-assistant ·949

Related clusters

Coq/Rocq Proof Formalization & Type Theory38 Cluster 63374028 Formal verification of cryptographic code22 Formal Mathematics in Rocq/Coq15 Cluster 6372245 Cluster 6338486

ejgallego/coq-lsp

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq…

OCaml

208

2,045 commits

rocq-community/rocq-lsp

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq…

OCaml

208

2,045 commits

ejgallego/rocq-lsp

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq…

OCaml

208

2,045 commits

LPCIC/coq-elpi

Rocq plugin embedding Elpi

OCaml

197

3,359 commits

AbsInt/CompCert

The CompCert formally-verified C compiler

Rocq Prover

2,227

2,436 commits

formal-land/rocq-of-ocaml

Formal verification for OCaml, with Rocq

OCaml

275

1,245 commits

clarus/coq-of-ocaml

Formal verification for OCaml, with Rocq

OCaml

275

1,245 commits

jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

Rocq Prover

365

4,570 commits

MetaRocq/rocq-verified-extraction

Verified Extraction from Rocq to OCaml/Malfunction

Rocq Prover

480 commits

yforster/coq-verified-extraction

Verified Extraction from Rocq to OCaml/Malfunction

Rocq Prover

480 commits

mit-plv/rupicola

Gallina to Bedrock2 compilation toolkit

Rocq Prover

812 commits

MetaCoq/MetaCoq

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

Rocq Prover

553

5,155 commits

MetaRocq/metarocq

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

Rocq Prover

553

5,155 commits

hacspec/hacspec-v2

A Rust verification tool

Lean

480

5,203 commits

octra-labs/amlc

amlc - applied meta lang compiler and local aml executor

OCaml

1 commits

cryspen/hax

A Rust verification tool

OCaml

480

5,061 commits

awslabs/aws-lc-verification

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

Rocq Prover

145 commits

hacspec/hax

A Rust verification tool

Rust

480

5,061 commits

rocq-archive/coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Coq

136

1,097 commits

ejgallego/coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Coq

136

1,097 commits

PrincetonUniversity/VST

Verified Software Toolchain

Rocq Prover

507

6,149 commits

CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

Rocq Prover

178

2,544 commits

mit-plv/fiat-crypto

Cryptographic Primitive Code Generation by Fiat

Rocq Prover

840

8,337 commits

mit-plv/rewriter

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

Rocq Prover

5,807 commits

mit-plv/kami

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

Rocq Prover

170

598 commits

mit-plv/bedrock2

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

Rocq Prover

336

3,631 commits

garrigue/lablgtk

LablGTK 2 and 3: an interface to the GIMP Tool Kit

OCaml

404 commits