Byte Repair uses formal verification to prove no bug slips through, and regression verification to prove your next change doesn't bring one back. Every path, both versions, open source.
The institutions Byte Repair’s work is affiliated with.
University of Manchester
Founder's Institution
University of Lancaster
CyberCom Host InstitutionThe Byte Repair Enterprise Server has received support from the North West CyberCom project, a Research England funded initiative to transform cyber security research into innovative commercial solutions.
Byte Repair’s mission is to protect you from tomorrow’s vulnerabilities and from the changes that quietly reintroduce yesterday’s. Formal verification finds bugs testing tools can’t; regression verification proves a fix or refactor doesn’t break what was already working.
Parse any verifier output.
An extensible framework and library that parses the output of verifiers and testing tools. Has builtin support for ESBMC, CBMC, Clang, Kani and PyTest so you write a parser once instead of once per tool.
Learn MoreYour private everything assistant. With Byte Repair inside.
An open, private, client-side LLM assistant that runs on your own machine and talks to your own model endpoints. Your code, created automatically, verification-backed.
Learn MoreVerification and repair for your whole team, wired into your git host.
A server that mirrors your repositories, verifies every pull request, and opens its own pull requests with proven repairs.
Learn MoreByte Repair does the same things everywhere it runs, whether that is a library call on your laptop or a server watching your pull requests. Two pillars carry the weight: formal verification finds what’s wrong, regression verification proves a change doesn’t make it worse.
Formal verification does not sample inputs; it reasons about all of them. Byte Repair breaks a codebase down and verifies each function individually, so the method scales past the point where whole-program analysis gives up. It drives industry-tested verifiers underneath: ESBMC, CBMC, and Kani.
Finding bugs is one job; proving a change doesn’t reintroduce them is another. For each changed function, Byte Repair builds one harness that calls both the old and new versions on the same nondeterministic input and discharges a conditional-equivalence proof: where the old version was correct, the new one must match it; where the old version was wrong, the new one must be correct. A verdict is only reported when the proof holds, and state the harness could not compare surfaces as unknown, never a silent pass.
Finding a bug is only half the job. Each verified bug is routed to an LLM agent to produce a fix, and the fix is re-verified against the same proof. If the repair does not hold, it goes back to the agent. The loop only closes when the math agrees.
Nothing is rewritten behind your back. Your source stays where it is, and any change that touches code asks for your approval before it runs.
None of it runs on our servers, either. formal-lib is a library in your own process, Entoli runs on your own devices against your own model endpoints, and the Enterprise Server is installed inside your own network. Different reasons (portability in one case, compliance in the other), but the same answer to where does my code go: nowhere.
| Feature | Byte Repair | AI Agents (Claude, Codex, Gemini) | Snyk | SonarQube | Coverity |
|---|---|---|---|---|---|
| Formal Proof of Bugs | ✓ | ✗ | ✗ | ✗ | ✓ |
| Exhaustive Path Coverage | ✓ | ✗ | ✗ | ✗ | ✗ |
| Proves Changes Preserve Behaviour | ✓ | ✗ | ✗ | * | * |
| Automated Repair | ✓ | ✓ | ✓ | ✓ | ✗ |
| Safety-Critical Ready | ✓ | ✗ | ✗ | ✗ | ✓ |
| Agentic Integrations | ✓ | ✓ | ✗ | ✗ | ✗ |
*SonarQube and Coverity surface regression detection (diff-based scanning and build comparison), but neither discharges a conditional-equivalence proof between two versions of a function.
Verification tools ask you to trust their results. That is easier when you can read them. Byte Repair develops in the open under the AGPL-3.0, so the analysis running against your code is code you can audit, fork, and run yourself.
Where the AGPL does not fit (proprietary products, closed distribution), a commercial licence is available through UOM Innovation Factory, the commercialisation subsidiary of The University of Manchester. Licensing differs per project; each product page states its own terms.
Meet the team behind Byte Repair’s approach to automated code analysis, testing and repair.
Scientific Lead Advisor
Full Professor at the University of Manchester leading the Systems and Software Security Research Group. Internationally recognized expert in formal verification with 50 awards from software verification competitions and 170+ peer-reviewed publications.
Visit Website
Lead Developer
PhD student at the University of Manchester researching automated program repair using LLMs and formal methods. Lead author on work towards regression verification and automatic repair of software via large language models and formal verification.
Visit WebsiteStay updated with the latest developments in automated code analysis and our journey toward safer software.
Byte Repair is the first tool to formally verify the ESBMC Operational Model; work that will improve ESBMC's accuracy and reduce false results from edge cases.
Read MoreWe are going to visit and present at Climb UK.
Read MoreHelp us protect the world's most critical software from the next major vulnerability.
