AI-Assisted Formal Verification of Robotic Control Systems

When a robotic arm moves near a human, "we tested it and it worked" is not enough. Formal verification produces machine-checked proofs that a system satisfies its safety guarantees for all possible states, not just the ones you happened to try. This project asks one concrete question: can AI assistants meaningfully speed up the writing of formal proofs in control theory and robotics? To explore it, the project develops a Lean 4 library of machine-checked theorems covering stability, controllability, manipulator kinematics, and safety invariants. Around it, focused experiments are used to test whether AI tools reduce the time from a theorem statement to a proof that Lean 4 actually accepts. The central idea is that AI can help, but only within a tightly scoped domain and only when Lean 4 has the final word on correctness.