Haladir Thinks the Next Frontier of AI Is Not Intelligence but Judgment

The Macro: LLMs Are Smart but They Cannot Optimize

Large language models can write poetry, summarize legal documents, and generate code. What they cannot do is solve a constrained optimization problem with mathematical guarantees. Ask an LLM to find the optimal truck routing schedule across 500 delivery points with time windows, weight limits, and driver hours constraints, and it will give you something that sounds reasonable but is provably suboptimal.

This is not a knock on LLMs. It is a fundamental architectural limitation. Neural networks approximate. Formal solvers prove. The operations research community has spent decades building tools like CPLEX, Gurobi, and open-source alternatives that can find mathematically optimal solutions to constrained problems. But these solvers are hard to use, require expert formulation, and do not integrate well with the natural language interfaces that modern users expect.

Haladir, backed by Y Combinator, is an applied AI product lab that sits at the intersection of these two worlds. They combine SMT/SAT solvers, mixed-integer linear programming, operations research methods, and formal verification with LLMs to tackle decision-making problems that require both intelligence and mathematical rigor.

The Micro: Formal Methods Meet Modern AI

The founding team has four members. Jibran Hutchins serves as CEO, with Quan Huynh, Preston Schmittou, and Joseph Tso as cofounders. The team is building what they call “operational superintelligence,” which is a bold phrase but maps to a real technical approach.

Their research output includes ConstraintBench, a system for benchmarking and training LLMs on constrained optimization using solver-verified rewards. They also have RLFR, a project focused on training coding models with formally verified reward signals. Both projects attack the same core idea: making AI systems that can produce solutions you can mathematically verify.

The target customers are operations-heavy companies, think logistics, manufacturing, supply chain, energy, and defense, where decisions need to be both fast and provably correct. In these domains, a 2% improvement in route optimization or schedule efficiency can mean millions in savings.

Competitors include traditional OR consulting firms like Princeton Consultants and FICO (which owns the Xpress solver), as well as newer entrants like NextMV. But most of these either sell raw solver technology or custom consulting engagements. Haladir’s angle of combining solvers with LLMs for a more accessible interface is relatively unexplored.

The formal verification component is particularly interesting for regulated industries. If you can prove that your scheduling algorithm satisfies all safety constraints, that is a different conversation with regulators than “our neural network usually gets it right.”

The Verdict

Haladir is building at a genuinely interesting technical intersection. The combination of formal methods and modern AI is underexplored and potentially very valuable.

At 30 days: do they have a paying customer using the combined solver-LLM approach for real operational decisions?

At 60 days: how does their solution compare to pure solver approaches on standard OR benchmarks? Speed and solution quality both matter.

At 90 days: is the LLM interface actually making formal optimization accessible to non-expert users, or does it still require an OR specialist to set up?

I think the thesis is strong. Operations research is a massive, underserved market that has been waiting for better interfaces. If Haladir can make formal solvers as easy to use as asking a question in plain English while maintaining mathematical guarantees, they have something genuinely valuable.