SkyLabsAI/BRiCk

Formalization of C++ for verification purposes.

Rocq Prover

105

3,047 commits

updated Sep 23, 2026

skylabsai.github.io/BRiCk

See the code

README

BRiCk and other BlueRock libraries

Build

Follow instructions in the https://github.com/SkylabsAI/workspace meta-repo; that will checkout this repo and needed dependencies.

BRiCk (Program logic for C++)

See this README.md.

Code generator for BRiCk

See this README.md.

Lens library

See this README.md.

Extension of std++ for universe polymorphic monads

See this README.md.

Extension of the elpi standard library

See this README.md.

Extension of the Ltac2 standard library

See this README.md.

Ltac2 logging library

See this README.md.

OCaml library with extensions of the Rocq API

See this README.md.

OCaml logger library

See this README.md.

Extension of the OCaml standard library

See this README.md.

Instrumentation for the Rocq compiler

See this README.md.

coq

coq-formalization

coq-library

cplusplus

cplusplus-11

cplusplus-14

cplusplus-17

cplusplus-20

cplusplus-23

Contributors

1,998 commits

271 commits

153 commits

143 commits

Similar repos

bloomberg/crane

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid,…

167

mit-plv/bedrock

Coq library for verified low-level programming

MetaRocq/metarocq

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

554

MetaCoq/MetaCoq

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

554

PrincetonUniversity/VST

Verified Software Toolchain

507

coq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

rocq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

bloomberg/bde

Basic Development Environment - a set of foundational C++ libraries used at Bloomberg.

1,843

Languages

Rocq Prover

77.8%

C++

9.2%

OCaml

8.6%

Raku

1.1%

SkyLabsAI/BRiCk

Formalization of C++ for verification purposes.

Rocq Prover

105

3,047 commits

updated Sep 23, 2026

skylabsai.github.io/BRiCk

See the code

README

BRiCk and other BlueRock libraries

Build

Follow instructions in the https://github.com/SkylabsAI/workspace meta-repo; that will checkout this repo and needed dependencies.

BRiCk (Program logic for C++)

See this README.md.

Code generator for BRiCk

See this README.md.

Lens library

See this README.md.

Extension of std++ for universe polymorphic monads

See this README.md.

Extension of the elpi standard library

See this README.md.

Extension of the Ltac2 standard library

See this README.md.

Ltac2 logging library

See this README.md.

OCaml library with extensions of the Rocq API

See this README.md.

OCaml logger library

See this README.md.

Extension of the OCaml standard library

See this README.md.

Instrumentation for the Rocq compiler

See this README.md.

coq

coq-formalization

coq-library

cplusplus

cplusplus-11

cplusplus-14

cplusplus-17

cplusplus-20

cplusplus-23

Similar repos

bloomberg/crane

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid,…

167

mit-plv/bedrock

Coq library for verified low-level programming

MetaRocq/metarocq

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

554

MetaCoq/MetaCoq

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

554

PrincetonUniversity/VST

Verified Software Toolchain

507

coq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

rocq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources…

395

bloomberg/bde

Basic Development Environment - a set of foundational C++ libraries used at Bloomberg.

1,843

Contributors

1,998 commits

271 commits

153 commits

143 commits

Languages

Rocq Prover

77.8%

C++

9.2%

OCaml

8.6%

Raku

1.1%