Utility grant proposal

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.


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:

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|

1 Like

How many people in the community know what ForMet SubGov does?

I believe that quite many. We work in tough cooperation with both key stakeholders such as DeFi Alliance and EverLabs and other engineering sub govs such as DeFi and DevEx. This particular proposal was supported by key stakeholders before having been submitted. If you have some specific questions I’ll be glad to help you.

1 Like