Boogie: An Intermediate Verification Language

Ha, Spec#... Good old times... It has interesting static design by contract constructs as well as tracking resource ownership (via [Claims] attribute) 13 years before Rust! [0] Yeah, I know it's mostly apples to oranges but with Bartok [1] the CIL was compiled ahead of time to native code.

[0]: https://en.m.wikipedia.org/wiki/Spec_Sharp

[1]: https://en.m.wikipedia.org/wiki/Bartok_(compiler)