Mainframe Migration Risk: Why COBOL Behavior Cannot Always Be Proven

What is being proven

Legacy Lens does not attempt to prove that a system is safe, correct, compliant, or secure in the broad sense. Those are runtime properties that depend on environment, operations, and controls.

Legacy Lens proves a narrower property: whether specific behavioral claims are provable from submitted artifacts alone. The proof claim is about what the artifacts guarantee, and where they do not.

An authority record exists to document a decision that must survive scrutiny. If a decision relies on unprovable behavior, the organization inherits liability disguised as velocity.

Provability is binary

Many analysis products implicitly treat certainty as a gradient. They present scores, coverage metrics, and confidence levels. These are useful for engineering triage. They do not satisfy the post‑incident question.

Provability is binary because the existence of a single runtime‑dependent path is enough to invalidate a global proof claim. If any execution path depends on state that cannot be derived from artifacts, deterministic authority cannot extend beyond the boundary.

In a regulated context, a false GO is worse than a false NO‑GO. Legacy Lens is fail‑closed: it prefers refusal to unsafe approval.

The boundary classes that terminate provability

Provability boundaries are not rare edge cases. They are common patterns in production‑realistic estates. They include runtime‑mutable control flow, dynamic dispatch, transaction server control transfers, opaque binary exits, and missing external dependencies.

Each boundary is a statement about epistemic limits. It says: beyond this construct, behavior cannot be proven from the submitted artifacts alone.

• COBOL control‑flow mutation (ALTER; computed GO TO): the control‑flow graph is runtime‑dependent.
• Dynamic dispatch (CALL identifier): the call target is resolved at runtime and may not be enumerably bounded from artifacts.
• CICS error‑path opacity (EXEC CICS without RESP/RESP2; HANDLE CONDITION): control transfer and error behavior depend on region state.
• IMS DL/I runtime resolution: segment and PCB behavior depends on region state and database configuration.
• Assembler / opaque exits: behavior crosses a semantic boundary not represented in analyzable source.
• Unresolved externals: referenced behavior is outside the artifact set; authority cannot cover what is not present.

Why testing cannot replace proof

Testing answers the question: did this observed execution behave as expected? Proof answers the question: is any other behavior possible?

In estates with runtime‑dependent control paths, no practical test suite enumerates all possible states. A passing suite increases confidence, but it does not create a deterministic guarantee about unobserved paths.

Post‑incident scrutiny asks for defensible statements. If the institution cannot prove that a path is impossible, it must describe that limit plainly. Legacy Lens turns that limit into a replayable record.

What an authority record must say

An authority record must not predict outcomes for other systems. It must state what occurred under the declared governance context for the submitted corpus.

It must record the declared context as immutable, record the registry and policy fingerprint, and record the evidence bundle hashes that allow independent replay.

When provability terminates, the authority record must state termination as an evidentiary boundary, not as a defect claim.

• Declared governance context (locked before analysis).
• Registry version and policy hash (locked standard).
• Bundle root hash and findings hash (independent verification).
• Boundary disclosure: which boundary classes were detected, and where authority terminates.
• Explicit non‑claims: no runtime inference, no compliance certification, no remediation guidance.

How to use this pillar post‑incident

Post‑incident review is the hardest case. A regulator, board, or monitor asks not what was intended, but what can be proven. This pillar provides the definitional frame: where proof ends, authority ends.

It is appropriate to cite this pillar in board packets, examiner responses, integration diligence memos, and internal audit workpapers when the question is evidentiary rather than operational.

It is not appropriate to cite this pillar as a prediction about a third party estate. Legacy Lens publishes precedent; it invites comparison; it does not predict.

How to cite this research in an authority record

Use language such as:

This decision references Legacy Lens research (PILLAR_MAINFRAME_MIGRATION_RISK_PROOF). The analysis explains a provability boundary where deterministic guarantees collapse. Where provability terminates, authority terminates under the declared governance context.

Explicit non‑claims

• This research does not predict runtime behavior.
• This research does not certify compliance.
• This research does not recommend remediation steps.
• This research defines evidentiary limits only.