Yes you can run the syntax & model checkers from the CLI, although then you need to manually write the model-checking settings file which I don't think the video series covers. It is covered in Lamport's Specifying Systems book, or you can take a look at the settings file generated by the GUI toolbox and adapt it to your own uses.
