The following software tools are currently available, sorted approximately according to how recently they have been updated:

• Leon - Verifier and Synthesizer for Scala
• CVC4 - CVC4 SMT Solver
• Orb - Resource Bound Inference for Functional Programs
• Rosa - Compiler for Reals
• StringSolver - A solver for string transformations, file renaming and semi-automated bash commands.

• InSynth - Interactive Synthesis
• Pong Designer - Programming Games by Demonstration
• Eldarica - Predicate Abstraction Engine
• SmartFloat - Numerical Error Estimator
• Phantm - PHp ANalyzer for Type Mismatch
• Kaplan - Constraint Programming Extension of Scala, based on Leon
• Scala to the Power of Z3
• RegSy - Regular Synthesis over Unbounded Domains
• Comfusy - Complete Functional Synthesis
• UDITA Tool for Systematic Test Generation
• Nenofar - Negation Normal Form Automated Reasoner
• Jahob system

We believe many of these systems are already useful, even though their explicit goal was to explore and evaluate research results. If you consider some of them as toys, however, we will be flattered, because we believe that toys are at least as essential for the development of science and technology as they are for the development of children.

Two links to industrial-strength systems:

• http://typesafe.com/
• http://jasper-da.com/