CVLR, pronounced "cavalier", is a set of Rust libraries that provide
verification primitives for Rust. We currently use it for writing formal specifications for Solana and Soroban smart contracts.
Examples of respective usage can be found [here](https://github.com/Certora/SolanaExamples) and [here](https://github.com/Certora/sunbeam-tutorials).