veriT relies on third-party software. These external resources are used either as libraries or as stand-alone applications. They are:

GNU MP
The GNU Multiple Precision Arithmetic Library is used to represent and manipulate numerical value. It is distributed under the GNU LGPL.
E
The E equational theorem prover is a first-order logic theorem prover based on the superposition calculus. It is used as a standalone application and must be installed on the computer where veriT is executed. It is released under the GNU GPL.

veriT is used or being integrated with other software, such as:

Rodin SMT Plug-in
Rodin is an Eclipse-based development environment for Event-B. The SMT plug-in for Rodin allows to use SMT-solvers to discharge proof obligations. It is still under development.
CRefine
CRefine is an editor that supports the formal development of concurrent object-oriented software in Circus by implementing a refinement calculus.
Bliss
Bliss is a backtracking algorithm for computing automorphism groups and canonical forms of graphs, based on individualization and refinement.
Saucy
Implementation of a symmetry-discovery algorithm.
PermLib
PermLib is a C++ library for permutation computations.

In early releases, veriT used the SAT-solver MiniSat to represent and manipulate the boolean structure of the formulas.