Programming language semantics prototyping tool

Question

Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness?

I'm asking this, because I'm reading a book on Alloy and it provides the exact functionality that I want, but for models expressed using relational logic.

I'm aware of Ott, but it does not have this sort of "model checking" capability, since it is focused on generating code for proof assistant systems.

Any reference on such tool existence would be nice.