First of all, thanks for a very interesting video! I have a question about the way invariants are implemented in Spec#. Traditionally (i.e., in Eiffel), invariants are only checked when you exit a method that was called from a different object, so you can break an invariant somewhere in the middle of a method or even have a private method that breaks an invariant every time. Was there any specific design issue that made you change the way invariants work and enforce them after every statement, which led to the introduction of the expose block?