Utility grant proposal
ForMet SubGov, 02/28/22
Executive summary
The current proposal describes the support for infrastructure projects being developed by the members of ForMet SubGov team. The program is designed to fund the projects important for improving the quality and speeding up the formal verification of Everscale smart contracts as well as its core elements.
Motivation
Currently the formal verification, while being critically important for the Everscale community, meets a number of challenges that need to be addressed, such as:
- Extremely long and expensive process
- Poor support for the languages used by Everscale
- Too comprehensive and difficult to understand formal specifications
- Lack of proven features
- Hardly understandable outcome of the verification process
To resolve the issues mentioned above the members of the ForMet SubGov issue their own infrastructure projects that are believed to be critically important for the community, so the ForMet SubGov considers their financing as a must for the success of the whole Everscale project.
As these projects are quite different from each other and based on the unique expertise of the initiators the ForMet SubGov considers the regular contest system as non-applicable for these cases in favor of a grant system. It’s strongly believed that such an approach ensures the most effective way of development and adoption of such projects.
Grant rules
- All the projects supported by the ForMet SubGov form a Grant Pool
- Each project has a fixed quarterly budget (in EVERs, upon introduction of NEVERs they can be recalculated into the latter coin)
- Grants are paid in advance, once per quarter, starting from March 1, 2022, every three months
- The initial Grant Pool is defined in the present document
- For the upcoming payments each project must be reapproved by the ForMet SubGov
- For the reapprovement ForMet SubGov MAY require a report, either written or vocal, upon the ForMet SubGov decision about the activity for the past period
- Any project can be excluded from the Grant Pool either upon the initiator request or by ForMet SubGov decision (made as a Formal Proposal)
- Any initiator can issue a Formal Proposal to change the quarterly amount and ForMet SubGov can either accept or reject the proposal
- Anybody can apply for including their project into the Grant Pool using one of the following channels:
- Telegram group ForMet SubGov Community Chat
- Telegram group Formal Verification SubGov Everscale
- Forum at Formal verification section
Initial Grant Pool
| Project | Initiator | Short description | Address | Quarterly funding |
|---|---|---|---|---|
| Ursus | Pruvendo | Smart contract language as a DSL upon Coq with direct and reverse translators from/to Solidity and C++ (and possibly Rust) | 0:2a13be6dc3b58b9c9654b3a78d011b4d6df597d6b26e184e27a91d2eef17e850 | 400 000 |
| Soleil | OCamlPro | Why3-based deductive framework, with automated translation between Solidity/C++ and WhyML | 0:24a44423bc7edc2598b50ae87267bd06bc53455328e837dae32b9b7592716de7 | 400 000 |
| Everscale Verification Framework (EVF) | Infotecs | “Write spec, receive proofs for free!” |
EVF is a user-friendly Formal Verification framework for EverScale
smart-contracts (Solidity/C++), tailored specifically for both
functional-level and global system-wide safety/liveness properties
verification, backed by the modern Dafny automated proof system.|0:ef3813861e4717bc5b34bbdc13b3498ad2b0198100f87b9fa28cd080854c4ad8|400 000|