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 — ship it only when it's proven right. And shrink the math inside on-device AI so it runs faster and cheaper.
Prove that every change to critical code changes nothing it shouldn't. Works fully offline, inside your walls.
The routines that checksums, signatures and money depend on — proven identical after every optimization.
Smaller firmware, longer battery, cheaper hardware — with a proof that behavior didn't change.
Squeeze more out of every core you ship — verified separately for each target you sell.
One config line in your editor, one gate in your CI. Merge on PROVEN; get the exact breaking input otherwise.
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.