The modern world abounds with cyber-physical systems: Software controlling reality, from aircraft and self-driving cars to nuclear plants and smart grids. A big challenge today is how to make these systems correct and safe so that society can reap their full benefits.
VeriPhy fills in one piece of this puzzle. State-of-the-art hybrid systems proving can already rigorously verify rich safety properties of controls interacting with physics, and with a significant degree of automation. Until now, however, realizing strong safety guarantees at the implementation level has been the domain of humans: Guarantees can be automatically transported for weak modeling languages, but no prior tool for expressive models such as hybrid systems keeps correctness guarantees end-to-end. The alternative of implementing a hybrid model by hand is not only time-consuming, but prone to introducing bugs in software which absolutely needs to be correct.
VeriPhy changes that: not only can control software can be generated from safe hybrid models, allowing today's verification technology to see real-world use without the painstaking and error-prone work of implementing models by hand. That control software now comes with rock-solid correctness guarantees for each step of the generation process, crucial when the system being controlled is safety-critical. This verified control serves as sandbox around your existing control software: your controller does whatever it wishes so long as it is knowably safe. When VeriPhy detects danger, it kicks in with provably safe fallback control.
VeriPhy is an automatic synthesis pipeline: Verified hybrid systems models enter one end and verified object files come out the other. The verified object files can then be linked with your favorite control software to form a complete system. Along the way, it transforms the model step-by-step to an executable:
Like all good pipelines, you don't have to see what happens inside VeriPhy unless you want to. Whether you look at them or not, VeriPhy produces formal, foundational safety proofs for every step of the process, culminating in an end-to-end safety guarantee: the real system only enters safe states according to the safety specification of the source model. The proofs include:
These proofs exploit an array of theorem provers (KeYmaera X, Isabelle/HOL, HOL4) in order to productively verify domains ranging from hybrid dynamical systems to real analysis and from word arithmetic to register allocation. To minimize the trusted base in the process, the KeYmaera X core is cross-verified in Isabelle/HOL; the resulting verified core is highly scalable and checks 10,000's of steps per second.
VeriPhy is available as an extension of the KeYmaera X theorem prover. The VeriPhy implementation is more experimental (and has more dependencies) than the rest of KeYmaera X, so it is not in the standard distribution. Here is a distribution of KeYmaera X with VeriPhy:Download VeriPhy
This version has been tested on Linux and Mac only and may not work on Windows. Please email us if you have trouble.
VeriPhy can be used at the command line:
java -jar veriphy.jar -codegen in.kyx -veriphy -out dir
Where in.kyx is a KeYmaera X file containing the model and proof for your system.
This file can be generated through the KeYmaera X Web Interface.
The output will appear in dir.
The first time you call VeriPhy, it will install dependencies for you.
Installing and calling VeriPhy can both take a few hours because the installer proves CakeML correct from scratch and VeriPhy runs CakeML inside the HOL4 prover on each invocation.
We have plans to speed up the process, but right now patience is the price of verification.
Linking the final executable can be done with standard tools such as gcc. Code is currently generated for the arm6 and x64 architectures:
gcc bot_ffi.cpp bot_arm6.S -o arm
gcc bot_ffi.cpp bot_x64.S -o x64
On the Web UI, VeriPhy can be accessed by first clicking "VeriPhy" on the main menu:
This will take you to the VeriPhy page, where you can enter the model file and model name you wish to synthesize, along with an output directory where the generated code will be stored. Please note the synthesis process takes a long time and in the present release, you will not receive UI feedback when it completes.
The best resource for detailed technical information is our publications. The main paper for VeriPhy is appearing at PLDI 2018. Many components of VeriPhy are extended versions of existing tools. For detailed information, see the websites for KeYmaera X and CakeML. Additional papers describe the cross-verification of KeYmaera X in Isabelle and the ModelPlex tool for correct-by-construction monitor synthesis.
We have written a tutorial for basic usage of VeriPhy. The tutorial is a work in progress and feedback is highly encouraged, especially if you encounter difficulties.
Here are the people who make VeriPhy happen:
We are always interested in talking to users and potential collaborators both for applications and the VeriPhy software itself. If you have control software that you want to verify but aren't sure where to start, we welcome your email. We care about our users' experience, and your feedback can make VeriPhy better for everyone.