This crate contains code for graphs (undirected and directed) verified from first principles using Verus. The graph specifications and proofs strictly follow those found in the classic text on graph theory by W. T. Tutte. The code only covers finite graphs for the time being.
The goal of the crate is to provide abstract graph types that other crates can refine their data structures to and accompanying proofs to help verify the correctness of operations on the data structures (e.g., insertion into a binary tree maintains the invariant of it being an arborescence).
This crate provides a devcontainer installed with Rust and Verus.
To verify the crate:
cargo verus verify -- --expand-errorsThis crate is still in the early stages of development, and we welcome suggestions and contributions from the community. If you are interested in contributing, please feel free to open and issue or a pull request.