本申请公开了一种SM4密码算法的形式化验证方法，所述方法包括：将SM4密码算法的算法参数定义为安全整数类型；其中，所述算法参数包括明文输入、加密结果、密文输入、解密结果、主密钥、密钥常数、轮密钥和s盒参数；确定基于F*框架的算法模块的初始堆，并在所述初始堆的目标缓冲区中添加所述算法参数；利用所述算法参数对所述SM4密码算法的轮密钥生成模块、加密模块和解密模块进行形式化验证，得到所述SM4密码算法的形式化验证结果。本申请能够在SM4密码算法实现过程中保证内存安全、避免受到时间侧信道攻击。本申请还公开了一种SM4密码算法的形式化验证系统，具有以上有益效果。