本发明公开了一种基于符号执行对智能合约功能属性进行形式化验证的方法及系统，通过合约属性解析将自定义功能属性的证明转化为可达性验证，提供一种利用符号执行自动化进行形式化验证的新途径，对属性断言进行等价转换尝试进行归纳证明能对可归纳性属性达到快速验证的效果，有效提高验证速度，对于不满足的功能属性能够构造对应的反例提高可用性，另外，将符号执行与抽象验证分离开，能够避免不必要的抽象降低符号执行的效率，保证了符号执行收敛的速度。本发明可以自动化对智能合约功能属性进行形式化验证并输出不符合的属性的反例，并通过对合约属性的预处理，可归纳性验证和迭代不动点法相结合有效提高符号执行可达性验证的效率。