Verification of KeYmaeraX's core in Coq
This repository contains a formalization of KeYmaeraX's core in Coq. It includes a formalization of the syntax, dynamic semantics, and static semantics of Differential dynamic logic (dL), as well as a formalization of Uniform Substitution. We have implemented (and verified the validity of) dL's Differential Dynamic Logic and ODE axioms. We have also implemented a proof checker to write and check dL proofs in Coq. Here are some useful links regarding this formalization:
KeYmaeraX sourcecode is available here.
The technical report about uniform substitution is available here.
If you have any question, please send an email to either of us (preferably Vincent). You can find our email addresses on the CritiX webpage.
This work is supported by the SnT and the National Research Fund Luxembourg (FNR), through PEARL grant FNR/P14/8149128.
Install and Dependencies
Our formalization compiles with Coq 8.7.1, which you can get through opam. Here's how to get started with opam. We're using opam version 1.2.2 and we're using OCaml version 4.06.0. You might have to switch the OCaml version in opam, using
opam switch. To get Coq through opam, you have to add the following repository:
opam repo add coq-released https://coq.inria.fr/opam/released
after that you can run:
opam install coq
We're editing files using the ProofGeneral Emacs interface for Coq. You can find ProofGeneral and instructions on how to install it here.
Here's what I've got regarding ProofGeneral in my .emacs.el file:
(setq coq-compile-before-require t)
We are using version 3.0.1 of the coquelicot library for real analysis. There is a .tag.gz archive in this repository (they don't seem to have a git repository). Just untar it to start using it. It requires ssreflect (we're using version 1.6.4). The best way to get ssreflect is through opam by running:
opam install coq-mathcomp-ssreflect.
If you've cloned this repository, you'll need to pull the submodules by running:
git submodule init
git submodule update.
Otherwise, if it's an archive you've got, they should be part of the archive (only the coq-tools directory for the archive).
To compile all files you can evaluate in all.v using ProofGeneral, which is going to compile our examples and their dependencies. Alternatively, you can run:
to generate a Makefile; followed by:
make -j n
(where n is the number of cores you want to use to compile the project). Make sure that you've pulled the submodules before you run
./create_makefile.sh, otherwise the dependencies won't be computed right.
If you want to use ProofGeneral, and you're not sure what to do, here's what you can try to do: open all.v using Emacs. If you've installed ProofGeneral as instructed above, the ProofGeneral logo should appear when you start Emacs. If not, something went wrong. If the logo does show up in your Emacs buffer, then go to the end of the file and hit C-c C-RET. Assuming that you set the
coq-compile-before-requirevariable to true, it should compile the file and all its dependencies.
If you want to try to prove something yourself, look for example at examples/example1.v.
This repository is organized into the following folders:
- coq-tools: a submodule containing some useful tactics
- syntax: syntax of Terms, Formulas, Hybrid Programs and ODEs
- semantics: static semantic, dynamic semantics as well as soundness of static semantics (coincidence lemmas)
- substitution: uniform substitution and its correctness, as well as uniform and bound variable renaming
- axioms: DDL and ODE axioms
- checker: sequent calculus and proof checker
- examples: examples of proofs that use our proof checker