Free TON to Complete Original TON Development
As part of the Free TON Roadmap, the community has set a goal to complete the original TON protocol documentation, which includes the TON whitepaper, the TON Virtual Machine description, the TON blockchain description, and the description of the BFT Consensus protocol. Together they are referred to as the “specs” of the original TON protocol description.
This is a major piece of the overall vision that undertakes to develop and fine-tune governance processes, further decentralization of staking, changes in gas calculations and distribution, additional cryptographic primitives, extensions to the virtual machine, and a whole lot more.
There are significant gaps in the C++ node implementation when compared to the original TON vision described by Dr. Nikolai Durov. Since continuous node development was abandoned, Telegram could not finish all of the deliverables promised in the original documentation. Now it is up to Free TON to complete what was started.
Mitya Goroshevsky, CTO of TON Labs and contributor to Free TON stated:
“This is a commitment on behalf of the Free TON community to complete the development of the original TON — rigorous process that will require many community members to take part and see this through to completion. The goal is clear and set. The commitment is evident.”
More detailed information can be found in the community forum here.
Pruvendo Joins Free TON to Provide Formal Verification
As part of this process, this past Tuesday, June 9th, during a Free TON weekly meetup live stream, the community members announced that Pruvendo, the leading formal verification technologies provider will be joining the network as a “bug killer”.
Pruvendo Co-Founder Sergey Egorov stated, “Traditional approaches intended to decrease the number of network bugs, such as intensive testing or external audits (a popular approach for validation of smart contracts on Ethereum) only bring partial success. While still important to catch defects, they are far from capable of eliminating risks such as the loss of major assets.”
Egorov went on to note several public cases where millions of dollars were either lost or put at major risk, including the $50 million DAO scandal, the Parity case where $150 million was frozen and underscored that hundreds of millions, even billions of dollars that are lost annually due to unmitigated software flaws.
“The real solution is to use formal verification based on strictly proven mathematics,” Egorov continued. “Similar to the way theorems are proven, so too can software be proven to work as intended.”
Pruvendo is a solution for formal verification of smart contracts specifically designed for Free TON. Based on the Coq theorem prover, often associated with its use in the transportation and aerospace industries, it has been adapted for blockchain applications to prove smart contracts that are written in the most popular programming languages and supports both high-level and virtual machine (assembler) level proofs.
Goroshevsky added:
The majority of today’s blockchains develop their own domain-specific languages (DSLs) for security reasons. As such, they are complicated to use and either hinder or delay technology sharing. From day one Free TON chose to use existing high-level languages. Pruvendo is an ideal match since they prove smart contracts written in those very languages while providing equal or better security. The Pruvendo solution will be used for verification of Free TON smart contracts as well as for proving parts of the blockchain itself, including the TON Virtual Machine and consensus algorithm.
For more information on Pruvendo please email them at team@pruvendo.com or contact Sergey Egorov on Telegram at @SergeyEgorovSPb.
