本发明公开了一种形式化验证系统，包括SEDS建模模块，用于依据电子数据表单规范文件建立SEDS模型；模型转换模块用于将SEDS模型转换为适合模型检查的形式化模型；性质规约模块用于对SEDS模型的功能逻辑的性质进行形式化描述；形式化验证模块用于对形式化模型和所描述的功能逻辑性质进行形式化验证，得到验证结果。本发明通过将SEDS模型转换为形式化模型，对SEDS模型的功能逻辑的性质进行形式化描述，对形式化模型和性质描述进行形式化验证，以从数学推理角度对SEDS的功能逻辑实现检查，进而保障软件的正确性和可靠性，同时用户还可以根据验证结果发现功能逻辑中存在的冲突或缺陷，并对SEDS模型中的错误进行修正。