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