2OBJ is a "meta-logical framework theorem prover", i.e., a system that can be tailored to prove theorems in any desired logical system, and can also prove theorems about proofs in that system.

2OBJ is built in top of the OBJ system. Logics are defined in 2OBJ by loading a suitable "frame" (a specification of a logics syntax and rules of inference) written in OBJ3. Once a frame is loaded users can then define and apply their own tactics (mechanised proof procedures) to build proofs over user defined theories.

2OBJ provides a convenient graphical user interface based on X Windows, and can be given a rigorous basis using universal algebra and category theory.