Equivalence Is Tiered, Not Binary
Static structure, module loading, runtime traces, visual states, and end-to-end flows cover different failure classes. One green tier cannot stand in for the others.
Two programs are not simply “equivalent” or “not equivalent” in a practical refactor workflow.
The answer depends on what was observed.
A static graph can show that exports and imports are preserved. It cannot show that a user journey still behaves correctly. A screenshot can show visual similarity. It cannot prove that a module loads under the candidate bundler or that an event fires once instead of twice.
KodeProof treats equivalence as an evidence ladder.
Cheap tiers catch broad structural failures
Early checks can validate source shape and module relationships:
- files and declared relocations;
- syntax and resolution;
- exported type and value roles;
- protected bindings and literals;
- direct consumers;
- new cycles;
- top-level effects;
- affected-test reachability.
These checks are fast enough to run often. They catch many refactor mistakes before a browser or full project build is needed.
Static analysis also has honest yellow outcomes. Dynamic imports, generated modules, unparseable syntax, or unavailable project configuration can leave evidence incomplete without proving a regression.
Module-load tiers exercise execution boundaries
A candidate module may parse while failing to load because of asset queries, CSS imports, workers, JSON attributes, aliases, package exports, or bundler-specific behavior.
A lightweight loader can emulate selected candidate build semantics in an isolated process. That emulation must be tested against the real bundler, not assumed.
Known unsupported classes—such as an untransformed glob or framework file requiring a plugin—should produce a coverage gap rather than a borrowed green result.
Runtime traces cover values and effects
Characterization can capture selected function calls, receivers, return values, throws, and side effects, then replay them against the candidate.
This catches changes static structure cannot see, such as:
- altered value classes;
- changed serialization;
- different mutation behavior;
- effects occurring after an
await; - identity-sensitive scene or state changes.
Trace coverage is still sampled. Unsupported values, truncated collections, unobserved calls, and missing continuations must remain visible.
Browser and visual tiers cover application state
Browser evidence can exercise routes, hydration, history, interactions, console errors, requests, styles, scene state, and selected visual observations.
It is stronger for the user-facing flow it covers and silent about flows it did not run. A parity report should retain the exact states, selectors, viewports, readiness signals, and exclusions behind the verdict.
Project gates remain their own layer
Typechecking, linting, unit tests, integration tests, and builds contain project-specific knowledge no generic verifier should pretend to replace.
They can also be baseline-red or environment-sensitive. KodeProof records their outcomes alongside structural and behavioral evidence rather than collapsing everything into one check mark.
Escalate in proportion to risk
Not every edit needs every tier. A documentation change may require formatting and link checks. Moving an initialization-sensitive module can justify static order proof, a clean build, module-load checks, and browser scenarios. A performance rewrite may need runtime traces and visual or interaction parity.
The change contract selects the required floor. A higher tier can add confidence but does not retroactively fill a missing lower-tier contract.
The verdict should name its blind spots
A useful equivalence result states:
- which tiers ran;
- which versions and environments they used;
- which states and symbols were covered;
- what was excluded;
- which gaps are known;
- whether coverage regressed from the baseline;
- which layer caused a block.
KodeProof does not use “equivalent” as a free-standing claim. It reports a bounded relationship between a before-state and candidate under a declared evidence stack. That narrower language is what makes the verdict actionable.