Solver/Prover list

Cool idea.  Here are a few more things that might be of interest.  Not all are code proof assistants, just listing extras in case serendipity.

https://github.com/Z3Prover/z3:  theorem prover from Microsoft Research

http://minisat.se/:  Compact and readable SAT solver

https://www.minizinc.org/:  MiniZinc is a free and open-source constraint modeling language.

http://alloytools.org/:  Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks

http://askra.de/software/prooftree:  A program for proof-tree visualization

https://www.cs.utexas.edu/~marijn/drat-trim/:  A proof checker for unSAT proofs

http://twelf.org/wiki/Main_Page:  Logic proof assistant

https://isabelle.in.tum.de/:  A generic proof assistant

https://tla.msr-inria.inria.fr/tlaps/content/Home.html:  Mechanically check TLA+ proofs

https://us.metamath.org/:  Interpreter for the metamath proof language

https://easycrypt.info/:  Computer-Aided Cryptographic Proofs

http://fmv.jku.at/picosat/:  SAT solver with proof and core support

https://github.com/higherorderco/kind:  A functional programming language and proof assistant

http://www.redprl.org/:  A proof assistant for Nominal Computational Type Theory

https://hackage.haskell.org/package/equational-reasoning-induction:  Proof assistant for Haskell using DataKinds & PolyKinds

https://hackage.haskell.org/package/equational-reasoning:  Proof assistant for Haskell using DataKinds & PolyKinds

http://hol.sourceforge.net/:  Interactive theorem prover based on Higher-Order Logic

https://github.com/ROCmSoftwarePlatform/hipSOLVER:  Interface to AMD rocSOLVER and Nvidia cuSOLVER

https://fmv.jku.at/lingeling/:  Fast SAT Solver

https://febio.org/:  tool for solving problems in nonlinear finite element analysis in biomechanics and biophysics

https://github.com/msoos/cryptominisat:  advanced incremental SAT solver

https://fmv.jku.at/cadical/:  Simplified CDCL (Conflict-Driven Clause Learning) Satisfiability Solver

https://github.com/ROCmSoftwarePlatform/rocALUTION:  Iterative sparse solvers for ROCm

https://github.com/sambayless/monosat:  SMT solver for Monotonic Theories

https://elpa.mpcdf.mpg.de/:  Eigenvalue Solvers for Petaflop-Applications

https://www.ibm.com/products/ilog-cplex-optimization-studio:  IBM Optimization solver for mathematical programming

https://github.com/coin-or/Cbc:  open-source mixed integer linear programming solver written in C++

https://www.princeton.edu/~chaff/zchaff.html:  Accelerated SAT Solver from Princeton

https://verit.loria.fr/:  Efficient SMT Solver

https://verify.inf.usi.ch/opensmt:  SMT Solver built on Minisat

https://yices.csl.sri.com/:  Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples.

https://computing.llnl.gov/projects/sundials:  SUite of Nonlinear and DIfferential/ALgebraic Equation Solvers

http://sat.inesc-id.pt/open-wbo/:  An open source version of the MaxSAT solver WBO

https://lpsolve.sourceforge.net/:  linear (integer) programming solver based on the revised simplex method and the Branch-and-bound method for the integers

https://www.labri.fr/perso/lsimon/research/glucose/:  Minisat-based SAT solver based on a scoring scheme introduced in 2009 for the clause learning mechanism of so called “Modern” SAT sovlers (see IJCAI’09 paper)

https://cvc5.github.io/:  An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems

https://alt-ergo.ocamlpro.com/:  automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat

https://boolector.github.io/:  Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions

https://github.com/coin-or/Clp:  Clp (Coin-or linear programming) is an open-source linear programming solver

https://fmv.jku.at/kissat/:  condensed and improved reimplementation of CaDiCaL in C.  It has improved data structures, better scheduling of inprocessing, optimized algorithms and implementation.  The solver is not incremental yet, but can be used as a library.

https://bitwuzla.github.io/:  SMT solver for bit-vectors, floating-points, arrays and uninterpreted functions

https://www.cs.utexas.edu/~marijn/drat-trim/:  DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs.

http://www.gprolog.org/:  free Prolog compiler with constraint solving over finite domains

http://ceres-solver.org/:  open source C++ library for modeling and solving large, complicated optimization problems. It can be used to solve Non-linear Least Squares problems with bounds constraints and general unconstrained optimization problems. It is a mature, feature rich, and performant library that has been used in production at Google since 2010

——

Found by searching Nix package db for “solver” and “proof”:  https://search.nixos.org/packages