1. Flyspeck
2. FPTaylor
3. Formal Verification of Nonlinear Inequalities
4. SSReflect/HOL Light
5. Interval arithmetic library in OCaml
6. SPARK
7. SPARK-PL

Flyspeck

A formal proof of the Kepler conjecture.

Author: Thomas Hales

• https://github.com/flyspeck/flyspeck/
• Old version
• Announcement of Completion

FPTaylor

A tool for rigorous estimation of floating-point round-off errors.

Author: Alexey Solovyev

• https://github.com/soarlab/FPTaylor

Formal Verification of Nonlinear Inequalities

A tool for formal verification of multivariate nonlinear inequalities in HOL Light.

Author: Alexey Solovyev

• https://github.com/monadius/formal_ineqs

• An older version distributed with HOL Light

SSReflect/HOL Light

An implementation of the SSReflect proof language in HOL Light.

Author: Alexey Solovyev

• https://github.com/monadius/hol-ssreflect
• Old version

Interval arithmetic library in OCaml

A simple interval arithmetic library in pure OCaml.

• https://github.com/monadius/ocaml_simple_interval

SPARK

A cross-platform free software for multi-scale Agent-based modeling.

Authors: Alexey Solovyev, Qi Mi, Maxim Mikheev

• https://github.com/monadius/spark-abm
• http://www.pitt.edu/~cirm/spark/

SPARK-PL

A programming language for rapid development of Agent-based models in SPARK.

Author: Alexey Solovyev

• https://github.com/monadius/spark-abm/tree/master/SparkLogo