- Isabelle is a generic proof assistant.
 - SCIP - Solving Constraint Integer Programs
 - Timefold
 - OptaPlanner
 - Jenetics
 - A Vehicle Routing Problem solver
 - Choco-solver
 - jMetal
 - OR-Tools - Google Optimization Tools
 - COIN-OR Foundation based Cbc (Coin-or branch and cut) is an open-source mixed integer linear programming solver written in C++
 - Theta contains an SMT solver interface.