Zot is an open and easily extendable bounded model/satisfiability checker. It was born as a satisfiability checker, as its original language is the TRIO metric temporal logic. Zot now supports operational, descriptive, or hybrid models. Its plug-in based architecture permits both mono- and bi-infinite discrete temporal domains (i.e., infinite both towards the past and the future), and also supports a dense-time variant of the MTL logic.