Formal verification of Vyper contracts

[nrryuya]

I've just started a project FVyper to formally verify Vyper programs with KEVM.

I want to discuss what kinds of program or contracts is good to be formally verified. Any feedbacks or comments are welcome!

This is my current roadmap.

Phase 1

Standards

• ERC20(DONE)
• ERC721(WIP)

Basic functions

• merkle proof checker (example impl, this might be built-in, #806)
• ecrecover (example impl, this might be built-in, #495 )

Phase 2

Basic contracts

• proxy (sol impl)
• multi-sig wallet
• crowdsale

Phase 3

Composable widgets

NOTE: "composable widgets" is not fixed yet, see the discussion in gitter

• ownership
• lifecycle
  • pausable
• state machine

Phase 4

• Integration to popular tools and frameworks (e.g. ethPM, truffle)

Future work

• Verify standards of Plasma and state channels after any standardization progress e.g. “Plasma Prime standard”)
• Verify S[NT]ARKs contracts
• Verify other token standards

[nrryuya]

About the verification of standards (e.g. ERC20 or ERC721), to verify both Solidity and Vyper contracts with the one specification would be a good way to make sure the compatibility.

[nud3l]

I think in phase 3, it would also be interesting to look at contracts that specify low-level functionality. BTCRelay would be an interesting example.

It provides SPV proofs for Bitcoin in Ethereum. What makes it interesting to me is that it uses the sha256 functions and requires bit-wise operations.

[jacqueswww]

@nrryuya great stuff! Let me know if there is anything you require from the vyper compiler side. The phases + contracts implementations look like a great start.

[nrryuya]

@jacqueswww Thanks! I feels like I should put a higher priority on "Composable widgets" or whatever makes it easier to reuse programs and patterns in Vyper instead of library or contract inheritance. It would expand the targets of this project and also a key for Vyper to be adopted more widely. (cc @fubuloubu @davesque)