This is an experimental framework to build practical, formally verified, cluster management controllers. The goal is to be able to write a controller in Rust, and have it be formally verified for correctness using the Verus toolkit.
You cannot compile the verifiable-controllers codebase with a standard rust compiler. You need to use the rust compiler supplied by the Verus project. Follow their installation instructions to do so.
- A Verus installation, using the
mainbranch
Set VERUS_DIR to the path to Verus
export VERUS_DIR=<path-to-verus>
To build and verify the zookeeper controller:
$: ./build.sh zookeeper_controller.rs -o zookeeper-controller
For Mac users, you might need to manually add ssl to LIBRARY_PATH to build it.
To deploy the verified zookeeper controller to a Kubernetes cluster:
$: ./deploy.sh zookeeper
This script will deploy the zookeeper controller image (hosted at our repo) inside your Kubernetes cluster.
Our verification approach is described here.
The verifiable-controllers project team welcomes contributions from the community. Before you start working with verifiable-controllers, please read our Developer Certificate of Origin. All contributions to this repository must be signed as described on that page. Your signature certifies that you wrote the patch or have the right to pass it on as an open-source patch. For more detailed information, refer to CONTRIBUTING.md.
This project is available under an MIT License.