ConCert
ConCert copied to clipboard
AU-COBRA
A framework for smart contract verification in Coq
I was looking into extracting the counter module to concordium, using our Wasm [backend](https://github.com/womeier/certicoqwasm) for CertiCoq. CertiCoq is currently on [MetaCoq 1.3](https://github.com/MetaCoq/metacoq/releases/tag/v1.3-8.17), which ConCert doesn't seem to work with. Do...
Hello everyone, As per my understanding Concert project is two main projects: 1- An verified extraction plugins from Coq to Rust Liquidity. 2- Verified block chain applications that use the...
After inlining has been added, the translation `(f "") -> f` is no longer necessary, so it should be removed.
The support of recursive functions of multiple arguments has been added to LIGO: https://gitlab.com/ligolang/ligo/-/issues/1248 The pretty-printer could be simplified because wrapping multiple arguments in a tuple is no longer required.
The *view* functionality allows for querying contracts in a synchronous way. This functionality makes it easier to implement contracts that require using some data from other contracts, for example, getting...
Both Tezos and Concordium have a concept of *entypoints* which we model as a `Msg` type, usually represented as an inductive type with several constructors corresponding to the entrypoints. However,...
Dexter1, Dexter2, and FA2 all use a deprecated FA2 interface, these should be ported to the new interface added in #164.
* Updates the MetaCoq dependency to version 1.3.1 * Support std++ 1.9.0-1.10.0 * Support Coq 8.17-8.19 Should not be merged yet as it includes temporary workarounds for the following issues:...