一种人机协作的证明方法，在Proof Assistant/交互式定理证明器中进行的形式化验证。一般而言需要某种用于程序性质的逻辑推理系统为基础，比如霍尔逻辑。IPA 内部可能会有自动化的证明策略，如结合 SMT 自动判定属于特定理论的片段。 See: Lean Rocq /Coq Isabelle