Researcher Geby Jaff directed ten Claude agents to produce C-HD and a Lean proof; its runtime claim applies to a limited range of graphs.
By [RuntimeWire Staff](https://runtimewire.com/author/runtimewire-staff)
· Published
Primary source: [Vals AI](https://www.vals.ai/blogs/faster-shortest-path-algorithm)
Why it matters #
Vals has published a checkable artifact from an AI research task rather than only reporting an agent score. The Lean proof supports a narrow asymptotic claim; practical speed and novelty still require separate scrutiny.
Rayan Krishnan (@RayanKrishnan) and Langston Nashold (@langstonnashold) built Vals AI to measure what AI systems can do. On September 20th, Vals published a different kind of test: researcher Geby Jaff said ten Claude Opus 5.5 agents had devised a shortest-path algorithm and produced a Lean proof of its correctness and runtime bound in about 15 hours. The claimed improvement is mathematical and applies to a specified range of graphs. It is not a measured speedup.
Krishnan and Nashold studied computer science at Stanford and worked together on measurement problems before starting Vals, according to Andreessen Horowitz's account of its investment. Krishnan had worked as a software engineer at Palantir; Nashold had worked at Hudson River Trading. Their commercial premise is that model buyers need evaluations grounded in actual work, rather than scores selected by the model makers. Jaff's project puts that premise under an unusually demanding test: the output is an algorithm whose stated guarantee can be checked against a public formal artifact.
Jaff described the experiment in Vals' research post. He assigned the agents roles and gave them a message board where they could exchange ideas, challenge proposed approaches and redirect their work. He reported 733 messages before they completed C-HD. He also instructed them to compare their result with recent research and obtain reproducible verification before claiming success. Those are Jaff's account of how the work was conducted, not a controlled comparison of agent teams with human researchers.
What the proof covers
C-HD addresses exact shortest paths from one starting point in a directed graph whose edges have non-negative real weights. If a road map were represented as vertices and weighted connections, the task would be to find the least-cost route from one vertex to every reachable vertex. C-HD is a deterministic algorithm for that abstract problem; Vals' claim concerns how its work scales as the graph grows.
The relevant yardstick is Dijkstra's algorithm, with a bound of O(m + n log n) using a suitable priority queue, where n is the number of vertices and m the number of edges. A 2025 paper and a 2026 follow-up established other deterministic bounds for directed shortest paths. Jaff's comparison selects a graph-density range where the published results leave room for improvement. For graphs with roughly m = n(log n)^(3/4) edges, Vals says C-HD's proved upper bound becomes O(n(log n)^(11/12)), against O(n log n) for Dijkstra. The smaller exponent establishes an asymptotic advantage for that comparison as n grows; it supplies no elapsed-time result for a real graph.
The method runs bounded searches from a frontier of discovered vertices. A newly encountered vertex can count against a local search limit even when the edge leading to it fails to improve a distance estimate. Search trees and pivots then organize subsequent work. The full stated bound charges operations beyond the searches, including sorting outgoing edges, reading the input and producing output. That accounting matters: a proposed algorithm can appear faster if preparation is treated as free. C-HD's certified density condition is m <= n floor((floor(log2 n))^(3/4)). Outside that range, the formal program uses a Bellman-Ford fallback rather than claiming C-HD's improved bound everywhere.
Vals has released the Lean proof package, including the theorem, an informal paper, build instructions and verification records. Its repository says the frozen project builds and proves the specified exactness and charged-runtime statements without remaining theorem hypotheses. That is a substantial, inspectable artifact. It also defines the limit of the claim: the proof establishes a theorem within its formal computational model. Assessing novelty against prior algorithms and whether the models being compared account for work in equivalent ways remains a task for algorithm specialists.
The distinction between verification and review is visible in Vals' own records. Jaff said he asked the agents for two reviews. The repository identifies one completed internal agent review and describes the second as provisional, with reproduction fields pending. Neither is outside peer review. Jaff reported small correctness simulations, but no benchmark on large real graphs; the repository warns that the formal construction has enormous constants. Vals' illustrative ratio of about 1.78 at n = 2^1000 compares leading expressions at an input size far beyond a practical test. It is not a claim that C-HD runs 1.78 times faster.
Why Vals published it
Vals normally sells the ability to evaluate models on work such as finance, coding and healthcare tasks. Its methodology says many of its test sets remain private to keep models from training on the answers. C-HD takes the opposite route for its central research claim: Vals has put the proposed result and formal files where others can inspect them. A proof-checked algorithm gives Jaff's experiment a sharper outcome than a self-reported agent success score, while leaving the claim open to scrutiny.
The publication follows Vals' August 13th announcement of a $40 million Series A at a stated $400 million valuation, led by Andreessen Horowitz. Vals named 8VC, Pear VC and Bloomberg Beta as returning investors, with HRT Ventures and Next Ladder Ventures joining the round. In that announcement, Krishnan said Vals' revenue had grown eightfold compared with all of 2025 and its customer count had doubled; Vals did not give the underlying revenue or customer figures in the announcement. The financing was an August event. The shortest-path research, published in September, is a separate demonstration of what an agent evaluation can yield, not a newly launched Vals product.
Krishnan has argued that tests must keep changing as models improve. In his Series A post, he described model development as climbing measurable hills and said evaluation makers were struggling to construct new ones fast enough. C-HD offers a concrete example of the difficult work Vals wants AI systems assessed against. Its public proof lets researchers examine the result; its narrow density condition and untested practical performance keep the conclusion proportionate to the evidence.