The full context for this work is presented on the author's blog.
This repo contains motivating examples for a Rust -> Oxide -> F* verification toolchain. The two main examples are in the folders
bloom-filter. Each one is a Rust crate that you can
cargo build or
cargo test, along with an F* implementation that you can
make verify or
To install F*, please follow the instructions here.