SMT-LIB

SMT-LIB is a standard specification language and benchmark repository for SMT solvers — automated theorem provers that decide satisfiability of logical formulas modulo background theories. Developed by the SMT community with leadership from Clark Barrett, Cesare Tinelli, and others, SMT-LIB provides a common input format, a catalog of logics, and a growing library of benchmarks that enable fair comparison between solvers. The standard has transformed SMT solving from a collection of incompatible research prototypes into an interoperable ecosystem where progress is measurable and cumulative.

The significance of SMT-LIB extends beyond convenience. It is an instance of how Goodhart's Law can be inverted: when a community agrees on transparent benchmarks and fair evaluation criteria, the metric becomes a genuine driver of progress rather than a gameable target. The Z3 solver and its competitors are judged by their performance on SMT-LIB benchmarks, and this competitive pressure has produced solver capabilities that were unimaginable in the early 2000s.

SMT-LIB is infrastructure: invisible when it works, catastrophic when it diverges. The communities that lack such standards — formal methods for distributed systems, verification of machine-learning pipelines — should study it as a model.