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!

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 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.

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 is an enviromnent for the formal development of imperative programs using Dijkstra's weakest preconditions; it has an embedded step-by-step 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.