package rocq-concert
A framework for smart contract verification in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.1.tar.gz
sha512=1ce7f7f45e51553b734b2cd40cd03bd61d6b58593b6ec503646f2cbb7517de6d4f9aa977c3c16bfb755d989cd33a50bc9dd88391ec87ceba7133bba7a1785050
Description
A framework for smart contract verification in Rocq
Published: 18 Mar 2026
Dependencies (8)
-
rocq-stdpp
= "1.13.0" -
rocq-elm-extraction
= "0.2.1" -
rocq-rust-extraction
= "0.2.1" -
rocq-metarocq-erasure
>= "1.5.1" & < "1.6~" -
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
>= "1.0.1"
Conflicts
None
On This Page