Formal Methods Sub-Governance Proposal

ForMet SG proposal


We hereby propose the creation of a Formal Methods Subgovernance (ForMet SG) for Free TON.

Mission and Vision

The mission is to facilitate the improvement of the software used on the FreeTON network by using formal verification methods.

The vision is to make FreeTON more secure and robust, and thus to enhance the FreeTON ecosystem and expand the FreeTON community.


The world of blockchain and crypto-currencies is a wonderful world for hackers looking for easy targets : smart contracts are small pieces of code managing huge amounts of crypto-currencies, and their automated behavior and immutability make them easy targets. The short history of blockchains is already full of stories of millions of USD stolen or lost in many smart contracts, starting from the DAO and ERC20 awful stories. Most of these contracts had been tested by developers (using frameworks like Truffle, etc.) and many of them were audited by “security experts”. Despite these efforts, there were still bugs to be exploited in them. This is due to the limited nature of such verification techniques.

On the other hand, formal methods provide much more bullet-proof verification techniques: they show that a smart contract code satisfies a formal specification, not for a few tested cases, but for all possible executions. This is a very strong property to get, that gives much more trust in the smart contracts than just testing or auditing. Yet, formal methods are limited by the expertise and skills required to deploy them on real life smart contracts.

The goal of this new sub-governance is to build a team of strong experts from various companies and to apply their expertise in formal methods to secure the Free TON ecosystem and its most important smart contracts.

Scope of Activities

The proposed sub governance shall perform the following activities:

  • Organization and running of formal verification contests
  • Distribution of funds to contest winners
  • Developing and improving the Free TON community guidelines on formal verification
  • Facilitating the development and application of open source tooling for formal verification purposes
  • Encouraging the creation of further formal verification teams

Formal verification is intended to be applied to the following software:

  • Smart contracts (especially those essential to the Free TON infrastructure)
  • TON compiler and other essential software
  • Other software related to the Free TON blockchain with critically important behaviour

Subgovernance Organization and Management


Initial Members




Public Key



Former Researcher in Prog. Lang. and Distr. Systems, CEO at Origin Labs, CTO at OCamlPro




Software manager/director with ~20 years of experience, Cofounder of Pruvendo




PhD. in Formal Proof ( using Coq. Engineer at OCamlPro/Origin Labs. Initial author of the Tezos Michelson formal proof framework in Coq and F*.




Researcher in the field of Formal Methods in Software. Pursuing PhD in Institute of Systems Programming (ISP RAS). Senior Researcher at InfoTeCS R&D (software security/reliability group). See my homepage.




Entrepreneur. Mathematician, Coq-programmer with 10+ years of experience. Co-founder of Pruvendo and




Programmer 30+ years of experience




Formal Verification Engineer, 8+ years of experience in Coq


The initial members shall oversee the efforts related to building the SG. They will also act as jurors until the SG jury is assembled.

Member Admission

Membership is open to everyone with proven experience in the field of formal verification, provided that a simple majority of the SG members approves the prospective member.

Membership Termination / Dismissal

Membership in the SG can be terminated at any time by notifying all members of the SG in the Telegram group.

A member can be dismissed from the SG if ⅔ of SG members cast their votes for this.


The communication on the matters related to the activities of the SG shall happen through the following channels:

  • Website on (publication of contest proposals, information on membership etc).
  • Forum on
  • Telegram group (open membership)
  • Regular (weekly/biweekly) call

Formal Verification Workflow

We hereby propose a workflow for formal verification. It comprises four phases, and each of them can be the subject of a separate contest. It’s illustrated at the next page and discussed further later.

Phase 1

  1. On the basis of information obtained from smart contract developers and architects (interviews, specifications, and source code), a semi-formalized specification in a controlled natural language is created.
  2. On the basis of the semi-formalized specification, a business-level specification is created so that:
  1. It is written in a natural language
  2. It contains a set of common-sense logical statements
  3. It is accompanied by diagrams and flowcharts
  4. It includes role-action matrices (optional)
  5. It includes a table of possible attacks and malfunctions prioritized by severity
  1. The business-level specification shall be reviewed and approved in due course by smart contract developers and architects.

Phase 2

  1. On the basis of smart contract source code, a formal specification should be provided  in a language that allows smart verification to be formally described. This language can be either the own language of the verification tool (proof assistant, Prolog etc.) being used or be a specific formal logic language such as:
  1. First-Order Logic
  2. Temporal logic of different kinds
  3. Separation Logic
  4. TLA+ family languages
  5. Reachability Logic
  6. Event-B

If need be, the source code can be translated to an embedded domain-specific language (eDSL).

  1. Using the formal specification, the functional verification is performed in one of the following ways:
  1. Semi-mechanical deductive reasoning (Coq, Agda, etc)
  2. Automated theorem provers (Vampire, etc)
  3. SAT/SMT solvers (Z3, AltErgo)
  4. Symbolic/Explicit Model-Checkers
  1. After review against the source code, the outcome is the code verified by a trusted proof checker so that:
  1. It proves the specification
  2. It is verifiable by an external trusted proof checker (e.g. Coq, Agda, Isabelle, Idris, K, whyML, Z3, AltErgo)
  3. The list of externally required specifications is kept separately for the sake of quick checkups
  4. The internal specifications and proofs are provided and fully pass the build chain
  5. All axioms (not proved assumptions) are kept in a separate file

Phase 3

  1. On the basis of the source code, the formal specification and functional proofs, the following artifacts are created:
  1. Scenario specifications
  2. Proofs of functional correctness
  1. The following verification is performed:
  1. Scenario-level verification
  2. Gas consumption verification
  3. Safety verification
  4. Liveness verification
  5. Verification of other requirements from Phase 1

Phase 4 (optional)

The goal of Phase 4 is to verify that the TVM code generated for the particular contract works identically to the source code verified at the former stages. Thus, the compiler will be verified but for the particular contract only. The kind of verification can be achieved, for example, by the following workflow:

  1. TVM bytecode is translated to an eDSL allowing for formal verification if needed
  2. Mapping between high-level state and TVM-level stated must be described
  3. The eDSL code is run
  4. The resulting state is translated to a form comparable with the initial state
  5. The states are compared, and the TVM bytecode is proved identical to the source code

Formal Verification Contest Organization

The SG shall follow the established Free TON practices when organizing contests.

The Jury

Contests are managed by the elected Jury. At the inception stage of the SG, the Initial Members shall organize the Jury Selection Contest; before the Jury is elected, the Initial Members shall act as jurors.

Selection Criteria

The Jury is elected from members with proven expertise in formal verification. Further requirements shall be described separately in the proposal for the Jury selection contest.

Some samples of Jury selection contest proposals for reference:

Functions of the Jury

The Jury shall perform the following functions:

  • Ensuring the smooth operation of the SG
  • Developing and reviewing contest proposals (CPs)
  • Accepting and reviewing contest proposals
  • Assessing contest submissions from participants
  • Choosing contest winners
  • Distributing funds between contest winners

Term of office of the Jury

Jurors are elected indefinitely; if a juror leaves the Jury, a new by-election contest shall be held.

Remuneration to the Jury

The matter is covered in the following section. Further details shall be included in specific contest proposals.

Budget and Remuneration

The global budget 

The global budget of the ForMet SubGov for 2021 can be summarized as follows:


1st place total award


Smart Contract Verification Contests

6.6 million TON

6 sets of smart contracts need to be verified (TIP-3, Elector, SMV, PBTG, Multisig v2, DePool 2)

Open Source Tooling Contest

1 million TON

Tooling to improve the quality of smart contracts in the ecosystem

TVM Verification Contests

500 kTON

2 contests: TVM formal definition and program logic for TVM bytecode

Bug Bounty Contest

500 kTON

Incentives for bug finders

TVM Audit Contest

300 kTON

Audit of the TVM Execution Engine in Rust prior to later formal verification

Specification contest

500 kTON

Contests for those parts of the system that are not planned to be formally verified in the near-term but still useful for the audit and other activities such as blockchain model, node model, consensus etc.

Bug Bounty

This is for the first place only, all the other distribution (second, third and other winning places) will be covered by the separate document as a function of the 1st place award and jury expected efforts. Normally jury bounty is 5% of the overall budget but for phases 2, 3 and 4 of Smart Contract Verification Contests it’s planned to raise it up to 20% as it requires extremely serious efforts.

Phase-by-phase breakdown (for Smart Contract Verification Contests)

It’s planned to keep the same 1st place awards as for the previous contests so:

Phase 1 : 50 kTON

Phase 2 : 350 kTON

Phase 3 : 350 kTON

Phase 4 (optional) : 350 kTON


total budget for this SG?

please include something like this, to get that easily processed

We request main gov to send X :gem: to 0:123...123

Hi! Thanks for the proposal. I would like to clarify the following points.

If need be, the source code can be translated to an embedded domain-specific language (eDSL).

This translation step is critical from semantic preservance viewpoint: it must be kind of sound, otherwise you risk introducing or loosing some behaviors. How are you going to ensure the soundness of this translation? Are the translation rules going to be published and/or peer-reviewed before taken as the verification target? Or is it a part of a contest submission and jurors are to establish soundness on their own?

Summary table needed:

How many TONs? When? For what (KPI).


Hi all,

Thank you for your comments, we tried to integrate all of them. Unfortunately, the new version of the proposal is too big to fit into the forum message so just providing a link: ForMet SG proposal v3 - Google Docs

With Best Regards,


Hi everybody, we did a lot but need to go further so asking for the second tranche (Stage Ib). The detailed report and description is below:

ForMet Subgov Stage Ib proposal


The current document is a request for the next tranche to ForMet Subgov (Phase Ib activity) as was approved by the Proposal #153.


Mission and Vision

The mission of the ForMet Subgov is to facilitate the improvement of the software used on the FreeTON network by using formal verification methods thus dramatically reducing the risk .

The vision is to make FreeTON more secure and robust, and thus to enhance the FreeTON ecosystem and expand the FreeTON community.

The details about ForMet Subgov activity can be found here with some updates provided here.

Completed contests

During the stage Ia the Subgov mostly worked on preparing the specific contracts for formal verification (as planned) as now we have three contracts that successfully passed Stage 0 (audit) and one - Stage 1 (formal specification). As a result we managed to find critical bugs in ALL the contracts.

Contest Description Status Amount
SMV Phase 1 contest Audit and formal specification for SMV Completed 110 000
Flex Phase 1 contest Audit and formal specification for Flex Completed 127 497
DuneSwap Phase 0 contest Audit for DuneSwap Completed 85 000
Radiance DEX Phase 0 contest Audit for Radiance-DEX Completed 63 752
SMV Phase 0 respin Reaudit of SMV as too many changes were introduced In progress 60 000

Expense sheet for Stage Ia

Enter balance 1 100 000
Contests completed 386 249
Transfer fee 3
Administrative fee 2 667
SMV Phase 0 respin 60 000
Exit balance 651 081

Phase Ib


Currently we are ready for starting real formal verification (Stage 2 - verification at functional level). Also we are about to start the formal verification of the node/VM itself (considering verification of Executors as a maiden project in this area). However, the time efforts for the formal verification are pretty big so need to ask for the next tranche (Stage Ib, as described in Proposal #153).

Rationale for amounts

In the past (see Contest #69) the overall cost of the Stage 2 contest was about 800K. This sounds as a reasonable amount for the project that typically takes 8-10 man-months of world-class engineers. However, the jury definitely has to be awarded better as it’s a time consuming activity of the top-ranked professionals so we propose to slightly increase the overall cost to 900K.

Regarding Executors we have a preliminary estimation that this activity will be slightly more time consuming than Stage 2 so the proposed overall cost equal to 1M looks reasonable as well.

Planned contests

Contest Description Amount required
Flex Phase 2 Formal verification of Flex at a functional level 900 000
SMV Phase 1 respin Updated formal specification for SMV 40 000
SMV Phase 2 Formal verification of SMV at a functional level 900 000
Executors Formal verification of Executors 1 000 000
Radiance-DEX Phase 1 Formal specification for Radiance-DEX 75 000
True NFT Phase 0 Code audit for True NFT 100 000
True NFT Phase 1 Formal specification for True NFT 100 000

The expected duration of Phase Ib is 3-4 months.

The requested amount

Item Amount
Amount available 650 000
Budget for contests 3 115 000
Administrative costs 16 000
Reserve 200 000
Required amount of tokens 2 680 000

This amount is less than a preapproved Phase Ib amount equal to 3 550 000.


Please approve the requested amount equal to 2 680 000 and send it to the subgov wallet 0:1ec958fd022ab1d479dd722283fe5fd1d9de7196ee7f09f96b68e435776548c1

1 Like