If you want a small stepping stone toward Versus, you can add Rust debug_assert for preconditions and postconditions; the Rust compiler strips these out of production builds by default.

Example from the Versus tutorial with verification:

    fn octuple(x1: i8) -> (x8: i8)
        requires
            -16 <= x1,
            x1 < 16,
        ensures
            x8 == 8 * x1,
    {
        let x2 = x1 + x1;
        let x4 = x2 + x2;
        x4 + x4
    }

Example using debug_assert with runtime checks:

    fn octuple(x1: i8) -> i8 {
        debug_assert(-16 <= x1);
        debug_assert(x1 < 16);
        let x2 = x1 + x1;
        let x4 = x2 + x2;
        let x8 = x4 + x4;
        debug_assert(x8 == 8 * x1);
        x8
    }