A hybrid formal verification tool for rust, based on symbolic execution

Context of the proposal:
VeriRust is a hybrid formal verification and automatic test generation tool for rust language. It leverages fuzzing and concolic execution exhaustively traversing paths in control flow graph, either hunting for bugs or automatically increasing coverage. VeriRust aims to providing a comprehensive verification tool for ink! smart contracts.

What VeriRust can do for smart contracts：

automatic vulnerability mining in smart contracts.
fuzz testing and formal-based coverage boost for the smart contracts.
fully formal verification integration with the ink! IDE or crate.
push-button solution for security testing of smart contract.

The current achievements in the research:
1. VeriRust runs on real-world Rust code with Standard Library. Below are statistics from testcases;
2. VeriRust online demo is available at : http://verirust.io .
3. VeriRust is based on 1.45.1-stable (c367798cf 2020-07-26).

Milestones (4 months):
1. Extract attack surface
Based on contract public API, write test harness for both fuzz testing and symbolic execution.
2. Build up contract testsuite
Collect enough smart contract test cases, make sure VeriRust runs correctly and satisfy the preset performance goals.
3. Optimize and release
Identify and remove performance bottleneck, integrate with popular Ink! IDE.
Cost : $25000
1. Servers & Devices:$3000
2. Employee payments: $ 22000

Treasury Proposal: 1080 DOT.
Assuming the current DOT valuation of 23$ we would commit to deliver the above for 1080 DOT.