ABSTRACT. We describe a new word-level model checking format to capture models of hardware and potentially software in a bit-precise manner. This simple, line-based and easy to parse format can be seen as a sorted extension of the word-level format BTOR. It uses design principles from the bit-level format AIGER and follows the semantics of the SMT-LIB logics of bit-vectors with arrays. This intermediate format can be used in various verification flows and is perfectly suited to establish a word-level model checking competition. A new open source model checker and bit-vector solver support this format. We further provide real-world word-level benchmarks on which these tools are evaluated.