本发明公开了一种基于形式化验证的嵌入式设备安全启动方案设计方法，基于形式化的分析与验证，通过分析威胁模型，得到安全需求，并以此为基础建立形式化模型，最终转换成安全启动方案，并通过定理证明的方法确保嵌入式设备安全启动方案的可用性和安全性，本发明针对嵌入式系统设备在安全启动过程中存在的安全性问题，提供了一种基于形式化验证的解决方法。该方法系统全面地分析了安全启动过程中所面临的问题，给出具体的安全启动方案设计，并通过使用定理证明的方法给出具体方案的可用性和安全性的证明，本发明不仅可以快速的解决安全启动过程中的威胁，还从理论上证明了方案的安全性和可靠性。