KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic (dL) and provides tactics for a high degree of control over automated proof search.
Sign in at the top of this page to get started online, or click 'Download' to install locally for improved speed.
Sign in at the top of this page.
This publicly hosted instance of KeYmaera X offers limited speed and is for demonstration purposes only. Use a fresh password when creating an account and do not upload anything to this server that is sensitive in nature.
Proof Tree
Proof Suggestions
Proof by Browsing
Proof by Pointing
Proof Found!
Model List
Model Details
