Mathematical programming formulations can yield faulty answers. Models can be unbounded, infeasible, or optimal with unrealistic answers. This article presents techniques for theory-based discovery of the cause of faulty models. The approaches are demonstrated in the context of linear programming. They have been computerized and interfaced using the General Algebraic Modeling System (GAMS), and are distributed free of charge through new GAMS versions and an outline web page.