Sibyl is an automated theorem prover for multi-modal hibrid logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies. It is based on a tableau calculus that is provably terminating and complete, provided that the negation normal form of the formulae given in input do not contain any occurrence of the binder that is both in the scope and contains in its scope a universal operator. The works lying Sibyl’s theoretical basis are cited in the Publications page. Sibyl is implemented in Objective Caml and runs under Linux. Some parts of its implementation code are inherited from its predecessor, Herod.