Isabelle theorem prover
Isabelle is a theorem prover for higher-order logics (HOL, ZF etc.). It is an integrated development environment for theories, proofs, and mathematical tools in Isabelle/ML (based on Poly/ML). System programming is done in Isabelle/Scala.
Platform: Linux, Windows, macOS
Poly/ML version: bundled
Licence: BSD and others
Download link: https://isabelle.in.tum.de
Project link: https://isabelle-dev.sketis.net