I took a skim and I like the ideas, but you should go further with proving elements of real systems. For example, drivers for Linux, if your whole goal is to prove these things while being a systems language. Although I confess that I don't understand its output, are you using a compiler backend like LLVM? Should be in README.