A Tscript program can be tested, like any other software system, to observe whether it exhibits the desired behavior. An alternative approach for analyzing communication protocols is model checking, which constitutes an automated check of whether some behavioral property is satisfied. This can be, roughly, a safety property, which must be satisfied throughout any run of the system, or a liveness property, which should eventually be satisfied in any run of the system. To achieve this, a Tscript program is first translated into a mCRL2 specification, from which the labeled transition system (LTS) is generated. Then, correctness properties are checked on this LTS using either mCRL2 or CADP. This approach has been applied on a standard example from the ToolBus distribution: a distributed auction system.