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.