In the past few chapters, we covered how to write complex specifications. However, our models have always been fairly crude: drop an operator or expression into Invariants and check that it’s satisfied. This is useful, but as you can probably guess by now, there’s also a lot more we can do with them. This chapter will cover some of the tools TLC provides to manage larger and more complex models.