Every 0, too. Binary Bedrock mathematically proves that changed code (an AI refactor, a compiler trick, a hand optimization) computes exactly what the original computed. Bit for bit, on all inputs. Not tested. Proven.
runs on-prem & air-gapped · your source never leaves your machine · zero model calls in the prover
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.
$ 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.
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 and runs every function through the
proof funnel automatically.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 $ ./bb verify-diff before/ after/
We publish what the tool measured, including what it can't do yet. That discipline is the product.
methodology & full runs available to beta partners · verdicts anchored in industry-standard formal tools (translation validation + SMT), independent of any AI model
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 ordinary refactors. 3.7% 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 · A Cortex-M4 routine made 59% smaller (34 → 14 bytes) and formally proven identical while shrinking.
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.
One config line in your editor, one gate in your CI. Merge on PROVEN; get the exact breaking input otherwise.
recorded run · Pointed cold at zlib + littlefs (219 functions, nobody hand-picked): 42 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.