The single-sphere driven balancing robot is an omnidirectional mobile robot, whose flexibility is particularly evident in narrow or complex environments. During the design of the kinematics and dynamics for this type of robot, it is crucial to ensure the correctness of the model. Traditional methods based on testing and simulation may not cover all system states and thus might fail to identify certain design flaws or potential safety risks. To ensure that the single-sphere driven balancing robot satisfies the correctness and safety verification requirements for safety-critical robots, a formal model of its kinematics and dynamics is constructed using the HOL Light theorem prover. The model is based on theorem libraries such as the real analysis library, matrix analysis library, and robot kinematics and dynamics library, and involves higher-order logic derivation and proof.