The single-sphere driven balance robot is an omnidirectional mobile robot, whose flexibility is especially apparent in narrow or complex environments. During the design of the kinematics and dynamics of this type of robot, it is important to ensure the correctness of the model. Traditional methods based on testing and simulation may not exhaust all system states, and thus might fail to identify certain design flaws or potential safety risks. To ensure that the single-sphere driven balance robot meets the correctness and safety verification requirements of safety-critical robots, this paper used the HOL Light theorem prover to construct a formal model of the kinematics and dynamics of this type of robot. The model is based on theorem libraries such as the real analysis library, the matrix analysis library, the robot kinematics and dynamics library, and carries out a higher-order logic derivation and proof.