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
To build and verify the controller examples:
$: VERUS_DIR=<path-to-verus> ./build.sh
To verify the tla toy examples:
$: <path-to-verus>/source/tools/rust-verify.sh src/temporal_logic_examples.rs
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.