Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata) Timbuk and reachability analysis can be used for program verification. For instance, Timbuk is currently used to verify Cryptographic Protocols (see some papers and in the examples of the distribution). Timbuk 3 is a fully new version of the tree automata completion engine used for reachability analysis. Older Timbuk distributions (2.2) provide three standalone tools and a bunch of Objective Caml functions for basic manipulation on Tree Automata, alphabets, terms, Term Rewriting Systems, etc.