NLCertify is a software package designed in OCaml/Coq for handling formal certification of nonlinear inequalities involving transcendental functions. The tool exploits sparse semialgebraic optimization with various maxplus/minimax approximation methods.