The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, possibly enriched with other logics (such as rewriting logic, hidden equational logic, or first order logic), and providing the powerful module system of parameterized programming...All the OBJ languages are rigorously based upon a logical system; more precisely, they are logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system.
The formal specification notation Z (pronounced "zed"), useful for describing computer-based systems, is based on Zermelo-Fraenkel set theory and first order predicate logic. Z is now defined by an ISO standard and is public domain.
ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation...All the ProofPower packages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License. (PPDaz is Ada stuff)
Jape is an interactive tool designed to help with learning, teaching and using formal reasoning. It takes a description of a logic as a system of inference rules, and supports the development of proofs in that logic.
R. Duke, P. King, G. Rose, and G. Smith. Technical Report, 91-1. Department of Computer Science, University of Queensland, St.\ Lucia 4072, Australia, (April 1991)