[FREE] Formal verification tool. Mathematically-proven 100% safe smart-contracts. Going viral on Twitter =)

scp1001 · May 5, 2019, 11:40pm

Formal Verification is the most powerful security conception in the world, there are only 2 Blockchains which already use it: Ethereum and Ziliqa.
This is not an absolute solution, but the nearest to 100% safety.

Outside of blockchain, just 30-40 companies use formal methods: for example, NASA, DARPA, Airbus, IBM, Apple.

Formal Verification allows to find all vulnerabilities in any smart-contract, or get the formal proof that contract is absolutely safe.
There are only 9 formally-verifified contracts in the world for now:

2019-02-27 GnosisSafe contract
2018-10-12 Uniswap contract
2018-07-12 Ethereum Casper FFG contract
2018-03-12 DappSys DSToken ERC20 token contract
2018-02-28 Bihu KEY token operation contracts
2018-01-30 MyKidsEducationToken ERC20 token contract
2018-01-26 OpenZeppelin ERC20 token contract
2018-01-16 HackerGold (HKG) ERC20 token contract
2017-12-23 Philip Daian’s Vyper ERC20 token contract

You can see more information about formal verification on reddit, with some comments of Vitalik Buterin, who is a huge proponent of those ideas.
It is unbiased discussion, where you can see advantanges and criticism of formal verification both.

I decided to start creating of such tools for another blockchains.
Waves matches perfectly: they have turing-uncomplete smart-contracts with limited complexity.
I called this tool Hyperbox, because it can process wide range of input and output values for smart contract in one launch,
instead of a single set in normal contract execution.

Hyperbox is a symbolic execution virtual machine for Waves RIDE smart-contracts, based on php, python and Z3Prover.
It mainly intended for formal verification and allows to find all existing vulnerabilities.
Hyperbox implements modern and powerful fully automatic multi-transactional search. For example, multi-transactional analysis support appeared in Mythril just recently:

Architecture Overview:

You can use Hyperbox on http://2.59.42.98/hyperbox/
It is free and open-source tool: http://github.com/scp1001/hyperbox
Version is 0.1, so syntax is very limited. It is just very early prototype, which was created during one hard week.

You can automatically solve predefinded crossing-river puzzle, or solve this smart-contract a bit lower as easy example (requires just 2 transaction).

Code:

let contract = tx.sender
let a= extract(getInteger(contract,“a”))
let b= extract(getInteger(contract,“b”))
let c= extract(getInteger(contract,“c”))
let d= extract(getInteger(contract,“d”))

match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,“a”))
let nb= extract(getInteger(t.data,“b”))
let nc= extract(getInteger(t.data,“c”))
let nd= extract(getInteger(t.data,“d”))

nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12

case _ => true

}

Also you can write and solve your own contracts using hyperbox.
Regular virtual machine is just a special case of symbolic VM, like cube is a special case of tesseract with 1 zero dimension. So Hyperbox can also be used as IDE for development and testing.

My article going viral, reposts on twitter: