package rocq-concert

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

A framework for smart contract verification in Rocq

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

T

The COBRA team

Maintainers

D

Danil Annenkov <danil.v.annenkov@gmail.com>

Sources

sha512=ab128a4dc0024ac19154dfa5bf6b16708464b4fb40b43fe26462c8ea323629e1dde569dfb63c30976d70a2741ae3d411d36315fec92c29c62a43ae97a8b793e0

Description

A framework for smart contract verification in Rocq

Published: 10 Mar 2026

Dependencies (14)

rocq-stdpp = "1.13.0"
rocq-elm-extraction = "0.2.0"
rocq-rust-extraction = "0.2.0"
rocq-metarocq-erasure >= "1.4" & < "1.4.2~"
rocq-metarocq-safechecker >= "1.4" & < "1.4.2~"
rocq-metarocq-pcuic >= "1.4" & < "1.4.2~"
rocq-metarocq-template-pcuic >= "1.4" & < "1.4.2~"
rocq-metarocq-template >= "1.4" & < "1.4.2~"
rocq-metarocq-common >= "1.4" & < "1.4.2~"
rocq-metarocq-utils >= "1.4" & < "1.4.2~"
coq-quickchick >= "2.0.4"
rocq-bignums >= "9"
rocq-stdlib >= "9.0" & < "9.1~"
rocq-core >= "9.1" & < "9.2~"

Dev Dependencies

None

Used by (1)

rocq-concert-examples

Conflicts

None

On This Page

Description
Dependencies (14)
Dev Dependencies
Used by (1)
Conflicts