The price of thought is plunging. The price of trust is not on the chart.

Epoch AI published "The Plunging Price of Thought" (Emberson and Roodman, September 22, 2026). The finding is striking: the cost of reaching a given benchmark score has fallen about 47% per quarter since 2023, roughly 13x per year. The method is careful. It prices the cheapest model that reaches each score, from math olympiad problems to PhD-level science questions.

Every benchmark in that study ships with an answer key: the correct answer is stored with each question, so a script grades a response instantly and at no cost. Grading is free. The price it tracks is the price of producing an answer.

Work does not ship with an answer key. Before anyone uses an output, someone has to establish that it is correct. We ran a study to put a number on that second price.

Trust is becoming the work itself. Boris Cherny, who created Claude Code, recently used Opus 5.5 to formally verify the Claude Agent SDK in Lean: a couple of short prompts produced 16 pull requests fixing bugs and race conditions. He combines Lean with TLA+ to look at data flow, concurrency and state, and asks whether formal verification is the future of bug finding. That is trust produced by machines instead of human reviewers, and it is the kind of checking this study prices. It also carries a condition: a formal model finds real bugs only if the model is faithful to the code, so the model has to be verified too. Our task is that step. A model reads the source of a real system and writes an executable model of it. On etcd Raft, Opus 5.5 produced a model that passed every check 6 times in 20.

Price per answer and price per verified answer

On the two small systems every one of the 160 specifications was verified. The price per answer and the price per verified answer are the same: $0.07 to $0.08 for Fable 5.1, about $0.03 for Opus 5.5, $0.003 to $0.004 for V4-Pro and under $0.001 for V4.1-Flash.

etcd Raft is different.

The price per verified answer is the expected cost of sampling until one specification passes every check. On the hard system it is 3.4 to 10 times the price per answer, and the ranking changes. Per answer, DeepSeek V4-Pro is 36% cheaper than Opus 5.5. Per verified answer, it is almost twice as expensive. V4.1-Flash stays the cheapest, but its advantage over Opus 5.5 shrinks from 7.7x to 3.7x.

The chart can be misread. V4.1-Flash gives the cheapest verified specification, but it is not the better modeler. Opus 5.5 reproduced all 97 recorded steps in 19 of 20 specifications; V4.1-Flash did so in 6 of 20. Opus 5.5 also answered in a median of 32 seconds, against 182 seconds for V4.1-Flash, which writes about ten times as many tokens. With 20 samples each, the difference in full passes (6 against 3) is not statistically significant (Fisher's exact test, p ≈ 0.45). V4.1-Flash is cheapest per verified answer for one reason: each attempt costs an eighth as much, and an automatic checker discards the 17 failures at almost no cost. Without a checker, a single V4.1-Flash specification has an 85% chance of being wrong, and a person has to find out which. A cheap model with a checker beats an expensive model alone. With no checker, the expensive model is the better choice.

Neither model dominates. Opus 5.5 copies the recorded behavior of etcd far more faithfully; V4.1-Flash keeps the safety invariants more often but diverges from what the real system did. Each fails a different check, which is another reason to run all of them. Highlighted cells mark the better value in each row; the difference in verified specifications is not statistically significant.

Price per answer also hides how the money is spent. Opus 5.5 writes about 3,500 output tokens per etcd specification. Both DeepSeek models write about 39,000, most of it reasoning.

The models fail differently too. 19 of 20 Opus 5.5 specifications reproduce all 97 recorded steps; 13 of them then violate a safety invariant when the state space is explored. 17 of 20 V4-Pro specifications fail on the recorded steps themselves. A single check would have told different stories.

Claude Fable 5.1, the most expensive model in the study, passed the machine checks most often when it answered: 4 of the 9 specifications it completed were verified, and all 9 reproduced every recorded step. But Fable 5.1 often did not finish. On 10 of its 19 attempts, Anthropic's API stopped the answer partway through and returned a refusal stop reason instead of a complete specification. We do not know why; the task is ordinary systems code. Each stopped attempt was still billed for the tokens generated before the stop ($0.39 to $2.06), so 44% of Fable's etcd spend bought nothing usable. A buyer pays for those attempts too, so they count: 19 paid attempts produced 4 verified specifications, $4.64 each, 6.3 times Opus 5.5. Counting only the finished attempts would give about $2.60.

What the checker misses

The checker missed 17 of the 35 planted bugs: 12 of 13 on the spinlock, 5 of 15 on the lock service, 0 of 7 on etcd. A typical escape lets a thread release a lock it does not hold. The recorded traces never contain that step, the invariants still hold, and the bug passes every check.

Every reviewer rejected every missed bug it reviewed: 17 of 17 for both DeepSeek models, 14 of 14 for Opus 5.5. They also rejected every bug the checker caught, and accepted all 120 correct specifications of the small systems they were shown, with no false rejection. On small systems the reviewer and the checker are complementary, and a reviewer costing a tenth of a cent did as well as one costing 2 to 3 cents.

"Verified" means consistent with what was recorded and with the invariants someone wrote down. It does not mean correct.

Limitations

• One task family (specifications of concurrent systems) and four models.
• 20 samples per cell (19 for Fable 5.1 on etcd, cut short by an API usage limit); pass rates are coarse and no significance test is claimed.
• Content-filter stops count as failed attempts at their billed cost. No reviewer saw the Fable 5.1 specifications.
• The cost of building the checker (instrumenting the systems, capturing traces, writing invariants) is not measured. It is the fixed cost behind the near-zero running cost, and token prices do not reduce it.
• The planted bugs were written by a model, and the reviewer prompt asked for faithfulness to the source, which is stricter than the trace contract.
• The Opus 5.5 reviewer did not see the DeepSeek V4-Pro etcd specifications or three of the planted bugs, and the V4-Pro reviewer did not finish the last five V4-Pro etcd specifications.
• API calls that failed during a network outage on our side were retried and are excluded from the prices.
• The study author designed the task contract (the lean executable-specification format used here).

Prices: Anthropic and DeepSeek list prices and AWS c7i on-demand rates, September 23, 2026.