AI Safety Research
- Major contributions to the KeYmaera X Theorem Prover for Hybrid Systems were supported by this grant:
- An initial public release of the KeYmaera X source code under a FOSS license, including the improved tactics framework and contextual equivalence tactics discussed in the grant proposal.
- Several subsequent public releases of the prover and its source code containing improvements resulting from watching students interact with KeYmaera X in the FCPS course.
- KeYmaera X source code is available at https://github.com/LS-Lab/KeYmaeraX-release/releases