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.