本发明涉及一种机械臂运动学形式化分析方法，包括如下步骤：步骤一，确定机械臂机构的结构参数；步骤二，用高阶逻辑语言建立机械臂机构运动学逻辑模型；步骤三，用逻辑公式描述需要验证的运动学约束或属性；步骤四，将机械臂机构运动学逻辑模型和需要验证的运动学约束或属性组成一个逻辑命题；步骤五，利用逻辑推理引擎证明所述逻辑命题是否成立，成立表明所述模型满足所述的约束或者具备所述的属性，否则，不成立表明所述模型不满足所述的约束或者不具备所述的属性。本发明中的形式化验证根据系统形式规范或属性，使用数学方法证明系统的正确性，对所验证的性质而言是精确和完备的。