Code Metal Proves Two Programs Are Equivalent. Nobody Asked What Either One Means
We would rather cite Code Metal as evidence than argue with it.
A $125M Series B into formal verification for defence is the single strongest piece of market proof that enterprises will pay real money to know whether code is correct. For two years the objection we heard most often was that correctness is a nice to have and nobody actually buys it. That objection is now settled, and it was settled by somebody else’s funding round rather than by anything we said.
Where we differ is on which version of the problem to attack, and Code Metal has been unusually honest in public about the cost of the version it chose.
What formal verification gives you
Code Metal’s approach compiles programs into an intermediate representation and then searches for a proof that a transformed program is semantically equivalent to the original. That is mathematical proof rather than statistical confidence. If the proof succeeds, the two programs behave identically, and no test suite anywhere gives you a guarantee of that strength.
For its target use case that is exactly right. Porting a kernel from one architecture to another in a defence context, where a subtle behavioural difference is not a bug report but a safety incident, is a problem that deserves proof rather than probability, and anyone offering probability there should be shown the door.
The ceiling they published themselves
Here is the part worth reading carefully, because it came from them rather than from a competitor looking for an angle.
Search time scales with program complexity, and pruning the search space by orders of magnitude was still not enough to keep it tractable. That is why the work is scoped to functions and kernels on purpose. It is not a roadmap item waiting for more compute to arrive. It is the shape of the problem, and equivalence checking has behaved this way for as long as people have attempted it.
There is a second property that matters more for our use case. The intermediate representation proves that two programs match. It does not say what either one means. Equivalence is a relation between two artifacts, and it is silent about purpose.
Why that is the wrong instrument for an enterprise estate
An enterprise runs hundreds of repositories holding somewhere between 10 and 100 million files. Agents now write most of the code going into them, the volume of change went up by an order of magnitude, and the number of people able to review it did not move at all.
The question that has to be answered on every change is not whether the new version is mathematically equivalent to the old one. It usually is not, because the entire point of the change is to change behaviour. The question is whether this change is correct when judged against what the rest of the organisation’s code already promised.
Consider a real example from a billing system. An agent adds a nullable field to a subscription model and stops counting cancelled subscriptions in monthly revenue. There is no equivalence to prove here, because the whole purpose is that the behaviour is different now. What matters is that the definition of an active subscription already lives in the billing package rather than the API layer, that the reporting service reads the same shape, and that a mobile client decodes the payload strictly so an unknown field fails the parse there. Four files need to change, and the fourth is the one an agent working without that knowledge would miss.
Proof cannot answer that, because the information required is about intent across repositories rather than about semantic equivalence between two versions of a function.
The practical version of the same problem
ByteBell attacks the practical version, which is checking a change against a derived specification with provenance attached to every claim.
Cheap open source models read every file once at indexing time. An agent detects the boundaries of each language element, stores them separately, and analyses each one in the context of its file, its module, its repository, and across every repository. For a single file the layer records what it does, why it exists in business terms, what users lose if it fails, the capabilities it provides, its edge cases, the contracts it provides, its preconditions, and the specific points where its behaviour is genuinely ambiguous. Everything is written in plain English with the file and the line attached.
Verification then means comparing a proposed change against what each touched file promised at the indexed base. We trace the impact, generate tests for it, run them, and review each modified file against its own prior commitment rather than against what the diff says it changed. Collateral damage is checked across the other repositories that read the same helper before anyone approves.
That is statistical rather than mathematical, and we are not going to pretend otherwise. It gives accuracy of code above 93% rather than a proof. What it buys in exchange is that it runs across a whole estate rather than a kernel, and that it costs something an engineering budget can absorb without a board conversation.
The cost profiles are not comparable, and that is the point
Formal verification inherits the cost profile of proof search, which is why it lives at function and kernel scale. Our indexing runs about $13 per 1,000 files, once, with only changed files re-derived on each commit.
On a traced run, tracing a change end to end across 32 impacted files in 4 repositories took 4 minutes 9 seconds and cost 30 for the same work by brute force. A full test generation and review pass came to 87,001 tokens at $0.11. Token spend drops by roughly 80% against reading raw files, which is how the layer manages to decrease AI cost while raising correctness rather than trading one for the other.
The reason those numbers are achievable is that we do the expensive reasoning once, before any question exists, on cheap open weight models rather than at query time on a frontier one. Proof search cannot be amortised that way, because each proof is specific to the pair of programs sitting in front of it.
Where proof is the correct answer
If you are porting a signal processing kernel to new hardware for a system where a behavioural difference could kill somebody, use formal methods and do not let anybody talk you into a statistical alternative. A figure of 93% is not something you want anywhere near a flight control surface, and we would say so in a sales meeting.
There is a real boundary here and it is better drawn clearly than blurred. Proof belongs to the small and critical. Derived specification and verification belong to the large and commercial. Most engineering organisations have both problems, and they are not solved by the same tool.
The honest limitation
Ours is a confidence figure and theirs is a guarantee, and no amount of accuracy improvement converts one into the other. A derived specification can be wrong about what code means, which is why every claim carries the file and the line it came from, so any statement can be checked in about 10 seconds. The layer also re-derives on every commit, and there is still a window after a push where a claim can lag the branch.
We also do not cover every language. Mojo is not indexed today.
This is what ByteBell builds
The useful reading of a $125M Series B into verification is not a competitive one. It is that a sophisticated buyer with a hard requirement decided correctness was worth nine figures, at function scale, in a single industry. The same requirement exists at estate scale across every industry, and it needs an instrument whose cost does not scale with proof search.
ByteBell is the verifiable context layer for code. We run the LLM compiler pattern, a one time pass where a model reads every file and lowers it into a verifiable code IR capturing purpose, business context and cross repository relationships, on your own infrastructure through Docker, with your source never leaving your environment. Every engineer, on any copilot, queries the same representation through a single MCP url, and every agent edit is checked against it before it lands, using per file SHA-256 diffing so only what actually changed gets examined again. Across 46 Kubernetes ecosystem repositories and 150,000 files we measured roughly 10% higher accuracy at 70% lower cost, on about a fifth of the tokens.