The Community Z Tools (CZT) project is building a set of tools for editing, typechecking and animating formal specifications written in the Z specification language, with some support for Z extensions such as Object-Z, Circus, and TCOZ. These tools are all built using the CZT Java framework for Z tools.
The Z machine is the largest X-ray generator in the world and is designed to test materials in conditions of extreme temperature and pressure. Operated by Sandia National Laboratories, it gathers data to aid in computer modeling of nuclear weapons. The Z machine is located at Sandia's main site in Albuquerque, New Mexico.
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.