To throw another one onto the _have you looked at X_ pile, Microsoft Research has put a lot of effort into the Why3 theorem proving platform, which is the backend for the verifier built into their (experimental?) verifier-aware, imperative language, Dafny[1]. It feels very much like writing C#/Java but with verified pre/post conditions, loop invariants etc.

I took a formal verification course in college that involved writing several verified sorting, search etc. algorithms in Dafny [2]. I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting.

(At the time I didn't realise that not only does the checker check the program, but compiles it into a CLR-compatible binary, hence you'll see equivalent C code for comparison)

[1] https://github.com/Microsoft/dafny [2] https://github.com/shawa/formal-verification-project