Formal verification of physical human-robot interaction using interactive theorem proving

Physical Human-robot Interaction ( pHRI ) involves physical collaboration between humans and robots to perform tasks safely and efficiently in shared environments. Traditionally, pHRI behavior has been analyzed using analytical or simulation-based methods, which may suffer from human error and incomplete coverage of system behavior. Formal methods, such as Interactive Theorem Proving ( ITP ), offer a mathematically rigorous alternative by constructing logical models of system dynamics and verifying their properties through deduction and proof. This paper proposes an ITP -based approach for the formal analysis of pHRI dynamics using the HOL Light theorem prover. We formalize the one-dimensional admittance control equations, derive their Laplace-domain representations, and conduct a formal stability analysis of the corresponding open and closed-loop controllers. To complement the formal verification, the verified open-loop admittance controller is implemented and simulated in MATLAB , where the step-response and root-locus analyses confirm the formally proven stability guarantees. The results demonstrate that the proposed framework provides both mathematical rigor and practical consistency for ensuring safe and reliable human–robot interaction.