http://doc.rust-lang.org/doc/rust.html#typestate-system
The way I understand them (and I say this a lot, but I could be wrong) is that it's like a more powerful version of Eiffel's design by contract, which allows the compiler to test whether invariants hold at compile time rather than just throwing assertions at runtime.
Another option (addon) would be to use commented invariants like in SPARK which are tested against the code by an automatic verification system even before compile time. To get an impression what it means, please read:
http://www.adacore.com/home/products/sparkpro/tokeneer/disco...
E.g. SPARK allows static verification of bounded memory usage, which I am not sure if rust's `check` is able to express.
AFAICT this requires forbidding recursion, unbounded loops and use of heap allocators or types/procedures which in turn have access to such facilities.
Or somewhat equivalently: the SPARK subset of Ada is statically verifiable by not being turing complete, so bits of the code can be verified, and elsewhere the full Ada language can be used.
I am not sure if Rust can emulate this.
(Again, I am not an Ada/SPARK developer so all of what I wrote may be wrong, do not take life decisions based on what I write)