I researched and discovered kani https://github.com/model-checking/kani, it's pretty cool.

```rust

#[kani::proof]

fn main() {

    let mut array: [i32; 10] = kani::any();

    array.sort_unstable();

    let index: usize = kani::any_where(|i| *i > 0 && *i < array.len());

    assert!(array[index] >= array[index - 1]);

} ```