  This paper reports on the development of a formal symbolic process virtual
machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security
of Ethereum-based services at the source code level of smart contracts, and a
Coq proof assistant is employed for both programming the system and for proving
its correctness. The current version of FSPVM-E adopts execution-verification
isomorphism, which is an application extension of Curry-Howard isomorphism, as
its fundamental theoretical framework to combine symbolic execution and
higher-order logic theorem proving. The four primary components of FSPVM-E
include a general, extensible, and reusable formal memory framework, an
extensible and universal formal intermediate programming language denoted as
Lolisa, which is a large subset of the Solidity programming language using
generalized algebraic datatypes, the corresponding formally verified
interpreter of Lolisa, denoted as FEther, and assistant tools and libraries.
The self-correctness of all components is certified in Coq. Currently, FSPVM-E
supports the ERC20 token standard, and can automatically and symbolically
execute Ethereum-based smart contracts, scan their standard vulnerabilities,
and verify their reliability and security properties with Hoare-style logic in
Coq. To the best of authors' knowledge, the present work represents the first
hybrid formal verification system implemented in Coq for Ethereum smart
contracts that is applied at the Solidity source code level.
