程序的形式化证明是指使用形式化方法来证明程序的正确性。其中，形式化方法是指在数学和逻辑基础上建立起来的，一套精确、严格的方法论。常用的形式化方法包括：Hoare 逻辑、抽象解释、模型检查、定理证明等。

其中，Coq 是一种广泛使用的定理证明器，它可以用于证明计算机程序、数学定理等各种命题。使用 Coq，可以构建出形式化证明，使得程序的正确性得到了数学上的保证。

Coq 中的形式化证明通常是通过构建一个逻辑系统来实现的。该逻辑系统包括一系列的公理和规则，以及用来表示命题的语言。使用这个逻辑系统，可以进行逻辑推理，从而证明一些命题的真假。

在使用 Coq 进行程序的形式化证明时，需要定义程序的语法和语义。通常使用归纳法来定义程序的语法和语义，并使用归纳法来证明程序的正确性。在证明过程中，需要使用 Coq 的逻辑系统来描述程序的性质，并使用归纳法来证明这些性质。

总的来说，程序的形式化证明是一种非常严格和精确的方法，可以保证程序的正确性。但是，由于形式化证明的过程比较繁琐，需要花费大量的时间和精力，因此通常只用于关键性质的证明。