Every 0, too. Binary Bedrock is the proof layer under your code: it mathematically proves that changed code (an AI refactor, a compiler trick, a hand optimization) computes exactly what it did before, bit for bit, on all inputs, and it hunts your existing repo for smaller code it can prove identical. Refactor away technical debt with a proof it changed nothing. Ship smaller binaries with the receipt attached. Not tested. Proven.
works with AI or without · any model, any agent, any workflow · hosted in minutes, or air-gapped on your metal where your source never leaves the building · zero model calls in the prover · every claim ships with a receipt you can re-prove
Give it two versions of a function: before and after any change. It compiles both and asks an SMT solver whether they are equivalent on every input. The answer is one of three, and it is never a guess.
The change is behavior-preserving. A machine-checked equivalence certificate is produced. Safe to merge. This is a mathematical proof over all inputs, not a test suite's sample.
The change alters behavior, and you get the counterexample: a concrete input where old and new disagree. The bug report writes itself.
The proof exceeded its budget. The gate stays closed: an unproven change is not treated as a safe change. Binary Bedrock fails safe, never silent.
Two qualifications exist and are always stated on the verdict itself: proofs over loops are conditional on the stated unroll bound, and domain-restricted proofs say exactly which inputs they cover. The verdict never claims more than the mathematics did.
$ bb verify-refactor crc_step.c crc_step_refactored.c ✗ DIVERGES: the rewrite CHANGES the behavior of @crc_step. Counterexample (an input where they differ): data = 0, crc = 10 Do NOT merge: the rewrite is not equivalent to the original. # the refactor looked identical in review. One character: >>4 became >>3. # a checksum every packet trusts. caught in seconds, with the input that proves it. $ bb verify-refactor bit_math.c bit_math_branchless.c ✓ PROVEN: the rewrite of @sign_branchless is behavior-preserving (bit-exact equivalent to the original, all inputs). A machine-checked equivalence certificate was produced. Safe to merge.
Point it at the code you already ship. It compiles every function, then three independent engines (the compiler's own pipelines, Souper's SMT synthesis, and a frontier model) hunt for smaller equivalents. Nothing any engine proposes is trusted: only candidates the prover certifies equivalent survive, and every win ships as a receipt (original, winner, proof, byte counts) you can re-prove with one command. Every function that could not be certified is listed with a named reason. No silent drops.
$ bb ingest compile_commands.json --target host --budget 60 submitted 111 · eligible 51 · proven equivalent 24 · wins 1 inflateValidate 11.2% smaller (89 → 79 bytes) wins/inflateValidate/ # zlib, audited cold. and you do not take our word for the win: $ bb verify-refactor wins/inflateValidate/original.ll \ wins/inflateValidate/winner.ll --budget 300 ✓ PROVEN: the rewrite of @inflateValidate is behavior-preserving (bit-exact equivalent to the original, all inputs). # the receipt re-proves on your machine. every audit win ships this way.
AI assistants write more of your code every week. Binary Bedrock is the gate they pass through: from your editor for single functions, or on your own hardware for whole trees.
verify_refactor and shows you
the verdict.{
"mcpServers": {
"binary-bedrock": {
"url": "https://mcp.binarybedrock.com",
"headers": { "Authorization": "Bearer <your-token>" }
}
}
}The demo endpoint verifies code you paste. It holds no keys, calls no models, and never executes your code. For anything sensitive, use the on-prem kit.
docker load, no registry, no account, no network required.bb ingest takes a source tree
or your build's compile_commands.json, cross-compiles for your real
target (--target cortex-m4; your build's own -mcpu flags
are honored), and searches every eligible function for a proven-smaller equivalent
with three independent engines: compiler pipelines, Souper's SMT synthesis, and a
frontier model. Every report says exactly which engines ran.bb verify-diff old/ new/ proves every
changed function across whole directory trees. One exit code decides the merge.$ sha256sum -c CHECKSUMS.txt # verify the bundle $ docker load < bb-toolchain.tar.gz $ ./bb ingest compile_commands.json --target cortex-m4 $ ./bb verify-refactor wins/f/original.ll \ wins/f/winner.ll # recheck any win $ ./bb verify-diff before/ after/
15 consecutive adversarial battery runs, 17,554+ recorded verdicts of deliberately broken code planted to fool the gate: zero false approvals. And the chain around the prover has its own battery: every pipeline defect we ever found is now a standing attack it must survive (latest run: 7 attacks, 0 false approvals). Re-run both yourself; they ship in the kit.
Every win, every proof, every claim on this site comes with an artifact that re-proves it on your machine with one command. You never take our word for anything.
Whole-function proving hits a wall fast: in our recorded sweeps the single-query approach exhausts its budget at 2 all-distinct components and is 152x slower at 512 repeated-kernel components. Both sweeps compose chains by construction, so the split points are part of the experiment design; automatic seam discovery on arbitrary code is the separately shipped and separately verified feature. Re-verified on the current toolchain this week.
We publish what the tool measured, including what it can't do yet. That discipline is the product. And it is enforced by a machine: every figure on this site is recomputed in CI from a ledger of the recorded runs, and the build fails if a published number drifts.
methodology & full runs available to beta partners · verdicts anchored in Alive2 (the LLVM community's translation-validation tool) and the Z3 SMT solver: peer-reviewed provers we deliberately did not build ourselves, with zero model calls in the proof path · every recorded campaign, repo by repo
Three verbs, every industry: reduce size, speed up, prove it didn't break.
Let AI write code, then ship it only when it's proven right. And shrink the math inside on-device AI so it runs faster and cheaper.
recorded run · We asked a frontier AI model for 126 refactors; of the 109 valid ones, 4 silently changed behavior. Every one was caught, none shipped.
Prove that every change to critical code changes nothing it shouldn't. Works fully offline, inside your walls.
recorded run · 17,554 sabotage attempts planted to trick the gate into approving broken code. False approvals: zero.
The routines that checksums, signatures and money depend on, proven identical after every optimization.
recorded run · A one-character typo in a CRC checksum (>>4 became >>3) was caught in seconds, with the exact input that exposes it.
Smaller firmware, longer battery, cheaper hardware, with a proof that behavior didn't change.
recorded run · littlefs, the most deployed embedded filesystem, audited cross-compiled ON Cortex-M4: 198 functions in, 31 proven, in the target's own bytes.
Squeeze more out of every core you ship, verified separately for each target you sell.
recorded run · The compiler's own vectorized rewrites of scalar routines went through the gate, each verdict anchored to a recorded solver run.
Refactor away technical debt with a proof it changed nothing; ship smaller code with the receipt. One config line in your editor, one gate in your CI. Then run the audit over what you already shipped.
recorded run · Pointed cold at zlib + littlefs (333 functions, nobody hand-picked): 67 proven, zero wrongly accepted.
Provers choke on big functions. Bedrock automatically splits code at safe boundaries, proves each piece, and proves the splitting itself, so proof time grows in a straight line instead of hitting a wall.
Request access below, or create an account directly. Once approved you create your own MCP tokens in the portal. We are onboarding a small number of teams: embedded & firmware shops, and engineering orgs using AI assistants heavily. You get a token for the editor demo, the on-prem kit, and a direct line to us. Bring a repo; the first audit report is the demo.