On November 16, 2018, Starteos — UESTC Blockchain Technology and Application Research Laboratory reported the first-stage formal verification research result at the Laboratory Office in Chengdu. Representatives of Starteos, UESTC and the Laboratory attended the reporting meeting.
(Professor Qian Weizhong is making a presentation)
(Starteos CEO Mr. Li Ang and Dr. Yang Zheng are discussing about Formal Verification)
● What Is Formal Verification?
Formal verification is to use logic to verify the reliability and feasibility of a program, i.e. to prove a program in a logical way to check whether it can get the expected results without any bug.
In the formal verification performed by Starteos — UESTC Blockchain Laboratory, the content to be proved is started with “Proof.” and ended with “Qed.”
If the content is proved successfully without any bug, “Qed.” will be highlighted in green:
If proving is paused manually, “Qed.” will be highlighted in red:
If proving fails, the error part will be highlighted in red and proving could not be continued:
In such situation, a detailed error report will be generated:
● The Advantages of Formal Verification
It will not be restricted by limited test sets and could logically summarize all the operating conditions.
Based on theorem proving, it supports infinite state sets and will not have false counterexamples.
It supports simulation of memory space and supports data structures such as pointer arithmetic and arrays.
It can greatly reduce manual abstraction and refactoring work, lowering the workload from 40:1 to 2:1.
Therefore, it will make developers more concerned with product design and can greatly improve the efficiency of design and verification while ensuring correctness.
● The Purpose of Formal Verification
To shorten and control the time and cost related with verification within a reasonable range.
To optimize the development mode of dApp.
Currently, there are already many formal verification projects based on Ethereum smart contracts, but the one based on EOS smart contracts has not been mature at this stage. Starteos expects the formal verification could serve not only EOS ecosystem but also the whole blockchain industry.
● Development Progress
The formal verification platform for Ethereum smart contract has been completed.
Different from the Solidity-based Ethereum smart contract, EOS smart contract is developed based on C++.
The initial work of the project focused on building some syntax in C++ that Solidity does not have.
It can be said that the preliminary work of the project is to expand the virtual machine for only Solidity into supporting both C++ and Solidity.
At present, the first stage of the formal verification project is near completion, and the second stage will be finalized next spring.
Telegram: https://t.me/starteos_io; https://t.me/joinchat/JOYkWE-IVr1Sno0yWevhxg
