Theona
I am a member of the Theona project, whose goal is to produce software tools and textbooks for the first two courses on programming. All the projects developed by Theona are free software. Feel free to ask for help if you want to hack on them!
 equ
 The goal of EQU is to assist the student to construct proofs for equational logic. You can download binaries or get the source code at github. The source code is split into a library (version 0.1) and the graphical interface.
 fun

FUN is an IDE with a strong emphasis on deriving functional programs from their specifications; the user can also prove that some program, already written, respects its specification. Since many derivations can depend on lemmas, FUN can also check proofs of mathematical statements. Get the binaries and source code for the libraries equ, fun, and for the graphical interface.
 sat
 The main aim of SAT is to help the student to grasp the semantic of formulas with quantifiers by using a signature with predicates denoting geometrical figures and relations about relative placements between the figures. Get the binaries (only for Debian/Ubuntu) and the source code.
 hal
 HAL is an enviromnent for the formal
development of imperative programs using Dijkstra's weakest
preconditions; it has an embedded stepbystep evaluator. Get the
source code for
the library and for
the graphical
interface.
Nota bene: Though I haven't been involved in the development of HAL, it is here for completeness.
Other stuff
Yahc is a checker for derivations in equational logic, but it is superseded by some of the programs in the Theona project.