https://www.absint.com/astree/index.htm

By the way, C has a formally verified C compiler:

https://compcert.org/compcert-C.html

On Astree, I couldn't believe it supported all language constructs. I found this on your link:

"and is subject to the same restrictions as Astrée for C.

The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatis­fac­tory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker."

So, it still does require a language subset that reduces complexity to benefit from the full analysis. They have greatly expanded what errors they catch since I first read about them. So, thanks for the link.

```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]);