Eliminating Redundant Axioms in KeYmaera X

KeYmaera X is a theorem prover based on differential dynamic logic (dL), which is tailored for the verification of hybrid systems that are common in the context of autonomous systems (e.g., autonomous vehicles, robots, etc). The basic idea is that KeYmaera trusts a small list of axioms (i.e., the kernel), and builds theorems using these axioms as building blocks, to prove more and more complex properties of dynamical systems.

Over the years, more and more axioms have accumulated in the KeYmaera X kernel, not all of which are strictly necessary, i.e., there are certain “redundant” axioms that can be proven using the other ones. The aim of this project is to identify and remove some of these axioms, replacing them with proof tactics. This can also be done with the help LLMs, offering the unique experience to use artificial intelligence to help with formal verification.

This topic assumes at least some familiarity with ordinary differential equations (ODE) and deductive verification, e.g., the applicant should have no problems with first-order logic or program verification.

For more information, please reach out to adrian.kulmburg@kit.edu.