  Blockchain technology adds records to a list using cryptographic links.
Therefore, the security of blockchain smart contracts is among the most popular
contemporary research topics. To improve the theorem-proving technology in this
field, we are developing an extensible hybrid verification tool chain, denoted
as FSPVM-E, for Ethereum smart contract verification. This hybrid system
extends the proof assistants in Coq, a formal proof-management system.
Combining symbolic execution with higher-order theorem-proving, it solves
consistency, automation, and reusability problems by standard theorem-proving
approaches. This article completes the FSPVM-E by developing its proof engine.
FSPVM-E is an extensible definitional interpreter based on our previous work
FEther, which is totally developed in the Coq proof assistant. It supports
almost all semantics of the Solidity programing language, and simultaneously
executes multiple types of symbols. FEther also contains a set of automatic
strategies that execute and verify the smart contracts in Coq with a high level
of automation. The functional correctness of FEther was verified in Coq. In
standard tutorials, the execution efficiency of FEther far exceeded that of the
interpreters developed in Coq.
