其理论基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上，寓于语言、技术和工具环境等形态之中。形式化方法是理论上保证计算系统正确性的唯一途径，是提高计算系统和应用的可靠性、安全性和可信性的重要方法。

早在1949年，A.M.图灵的论文“Checking a large routine”即讨论了程序的正确性问题。经过多年发展，形式化方法形成形式语言和形式语义学、形式规约、形式验证、形式化开发等密切相关分支。

形式语言是由符号化字母表以及递归的语法规则完全定义而生成之所有表达式或语句组成的语言。现代程序设计语言都是形式语言，而程序之含义的严格数学化定义则形成了形式语义学的内容，其方法有操作语义、指称语义、代数语义和公理语义。

形式规约使用形式语言刻画系统不同抽象层次的模型和性质。常见的形式规约语言包括表述数学结构（如代数结构、迁移系统）的模型规约语言和基于形式逻辑的（如霍尔逻辑、时序逻辑）的性质规约语言，而规约语言的语义都是在这些数学结构理论中定义的。

形式验证方法用来验证不同规约是否满足各类正确性需求，主要包括演绎式的定理证明、算法式的模型检验，以及构建在不同形式语义基础之上的静态分析方法（如抽象解释、符号执行）。定理证明在关于规约语言的形式推理系统中证明关于不同规约之间关系的定理，而模型检验用算法判定一个语义模型是否满足对应形式规约。

在形式规约和验证的基础上，形式化开发主要是构造、证明形式规约之间的等价转换和精化关系，以系统的形式模型和性质约束为指导，通过系统化搜索或逐步精化，综合、生成出满足需要的系统。基于模型的开发是形式化开发一种工程化表现形式。

形式化方法在实际场景下得到了诸多应用，例如硬件芯片的设计验证、操作系统和编译器验证和基于模型的安全攸关系统开发。形式化方法也是计算机科学和软件工程基本的认知方法学之一。作为一种方法学，形式化方法在人机物融合系统、人工智能、网络安全、量子计算、生物计算等方向的运用也受到了广泛关注。