Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them), the best choice depends on your particular case and specific needs.
Having that said, there are multiple (perhaps not so distinct) alternatives you might take (which includie the ones you've already mentioned):
- using a specific language/framework designed for creating and prototyping new languages: as an example, Redex [1], a domain-specific language embedded in Racket for specifying and checking (operational) semantics of programming languages, which, given a definition of a language, provides easy handling of tasks such as typesetting (in Latex), inspecting traces of reduction, unit tests and random testing (e.g. for checking typing)
- using general modelling languages that offer defining and performing certain analyses easily, as long as they can capture the specific language at hand to the needed extent; Alloy [2] is an example of such an approach: albeit pretty general and flexible, languages can be modelled as relations between states, while the support for model checking (e.g. evaluation within such language) comes for free after the semantics is expressed with a relation model (e.g. some ideas for modelling semantics of a language can be found in [3])
- embedding the language to check its properties using a theorem prover; an example would defining the language as well as its semantics by embedding it in a proof system like Coq [4] (more details about this approach, as well as discussion and demonstration of the difference between deep and shallow embedding in Coq is given in [5])
- using Ott (as already mentioned, with similar in spirit as Redex, but providing a new definition language rather than being embedded); Ott allows you to define the programming language in a convenient notation, and produce typesetting and definitions in a proof system (usually with deep embedding), where most of the checking (i.e. proof) needs to be performed manually
- developing the language and its semantics, as well as appropriate checks (e.g. as tests) "from scratch" in a general-purpose programming language and translation into other systems if need be, for checking purposes (some languages, like Leon [6], include built-in verifiers, which allow automatically proving certain properties and make this approach similar to embedding in a proof system)
Note that there is the trade-off between how easy is to use the framework/tool (e.g. as easy as laying out the definition on paper or in Latex) and how powerful the mechanisms for checking the properties about the language are (e.g. embedding the language in a theorem prover can allow checking very elaborate properties).
[1] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run Your Research: On the Effectiveness of Lightweight Mechanization. POPL, 2012.
[2] Daniel Jackson. Alloy: a lightweight object modelling notation. TOSEM, 2002.
[3] Greg Dennis, Felix Chang, Daniel Jackson. Modular Verification of Code with SAT. ISSTA, 2006
[4] Coq formal proof management system
[5] Formal Reasoning About Programs. Adam Chlipala, 2016
[6] Leon automated system for verifying, repairing, and synthesizing functional Scala programs
