It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
If I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.
