Verification frameworks

Verification frameworks: Dafny, Boogie, F*, VCC, Prusti, Creusot, Aeneas, Cogent, Rocq, and Isabelle/HOL, Versus (in Rust).

Typically they have syntax like:

exec_fn_item ::=

    visibility? exec? fn function_name generics?(args...) ( -> exec_return_type )?

        where_clause?

        requires_clause?

        ensures_clause?

        returns_clause?

        invariants_clause?

        unwind_clause?

I proposed adding some mathematical verification to C#, but failed:

 https://github.com/dotnet/csharplang/discussions/10306

For an example of proving LeftPad:   https://github.com/hwayne/lets-prove-leftpad