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：
1. automatic vulnerability mining in smart contracts.
2. fuzz testing and formal-based coverage boost for the smart contracts.
3. fully formal verification integration with the ink! IDE or crate.
4. 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.




VeriRust is a hybrid formal verification and automatic test generation tool for the Rust language which aims to provide a comprehensive verification tool for ink! smart contracts. It can do automatic vulnerability mining, fuzz testing and formal-based coverage boost. Currently, it works with real-world Rust code with Standard Library and an online demo is available. A milestones plan which further optimizes the tool and integrates with an ink! IDE is proposed with a cost of 1080 DOT.

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

No Active Proposals