PortProof: Semantic Backport Verification

Software teams often maintain multiple supported versions of the same product. When an important bug fix is made on the latest version, developers frequently backport that change into an older release. The problem is that the usual checks answer only part of the question. Git can report a clean cherry-pick and the target branch’s existing test suite can still pass, even when differences in the older architecture mean the behavior the original fix was supposed to introduce is still missing. PortProof verifies that missing semantic layer. IBM Bob 2.0 investigates the original source fix to reconstruct the public behavior the developer intended to preserve. A separate target investigation examines how the older release actually implements that behavior. Bob then maps the two, creates a structured BehaviorContract, and generates an executable proof through the target repository’s public interface. PortProof does not ask the AI to decide whether its own work is correct. Its deterministic verification core validates Bob’s structured artifacts, checks the declared public boundary, freezes the proof bytes with SHA-256, prepares an isolated target checkout, runs the repository’s existing tests, executes the exact frozen proof, and assigns one of three verdicts: PROVEN, NOT_PROVEN, or UNVERIFIABLE. If the behavior fails, IBM Bob can propose a bounded target-native repair. PortProof restricts what that repair is allowed to modify and then reruns the normal tests and the exact same frozen proof. This prevents the repair process from weakening the evidence simply to manufacture a passing result. The hosted demo demonstrates a zero-timeout backport where the checkout is clean and all existing tests pass, yet the expected value is 0 while the target still returns 5000. PortProof therefore returns NOT_PROVEN. After Bob proposes the repair, the same frozen proof observes 0 and PortProof returns PROVEN. PortProof is also a repository-oriented product rather than only a prepared demo. We independently validated its generic workflow on the real open-source korthout/backport-action repository, reproducing a documented historical fix. An older release passed its normal tests but failed PortProof’s derived behavior proof, while the corrected release passed the exact same frozen proof. The current hackathon release supports JavaScript and TypeScript Git repositories through a local CLI, with a constrained hosted experience for safe judging. PortProof’s core principle is simple: a clean cherry-pick proves the code moved. PortProof proves the fix moved.