The standard development tools for the Rust language provide a convenient mechanism for embedding tests within your code that can then be automatically run using the `cargo test` command. This video shows how to migrate from testing to verification of Rust programs by converting a standard Rust test to use Galois’ Crux tool. Crux can automatically ensure that tests will not fail for any possible input value of a given type, rather than the limited set of manually or randomly chosen inputs used for normal test suites. It exposes this functionality through a very similar `cargo crux-test` command. Here we demonstrate how easy it can be to adopt verification within a project by demonstrating Crux on a real-world cryptographic library, curve25519-dalek.
Learn more about Crux on our blog or at crux.galois.com