Introducing Parity: Prove what a replacement preserves

Replacing an old system is risky. The new one can look right while getting a small detail wrong. It might save an order twice. It might forget to send an update that another system needs.

A sufficiently detailed spec is code argues that a specification starts to resemble code as it gains enough detail to generate an implementation. During a legacy migration, we first have to learn what the old system does, specification can really help. Yet it can only include behavior we know to write down. With older, dark code, that poses an even harder challenge. Besides, if the spec starts to resemble code, I’d rather read the code at that point.

We are excited to introduce Parity, a verification tool built to prove which behavior a replacement preserves. A small language, and can automatically verify observed behavior between legacy and target.

LLMs accelerate software development. Code can look convincing, and an LLM will happily tell you it implemented every requirement. Engineers still need to verify that the change represents the original intent without regressions. Modernization makes this harder. We may not have written the original code, and its business rules may no longer be clear.

Teams learn small rules over years of running a system. Many of those rules never reach the prompt or specification.

It compares the old and new systems with the same inputs, including action responses and the views you define. Automatic audit adds supported process activity, network calls, database traffic, files, and state changes. Observed values must match unless the proof makes a difference explicit.

This goes further than checking the output a test author knew to assert. Automatic audit can expose behavior we did not know to put in the specification. Required audit stops when Parity cannot capture a supported effect well enough to compare it.

The language is built to live inside Markdown specifications and read like a testing scenario. Humans and LLMs can review and change it. Parity works across languages and architectures because it runs programs through command, process, or HTTP interfaces.

Parity is a development preview. The example in this article contains two working services built for this experiment. You can read the complete COBOL-to-Rust example.

Specifying our first scenario

We start with a specification in OpenSpec format for one scenario. We can use AI to help identify old behavior, while OpenSpec gives the team a document to review and change.

The service lets a customer reserve stock. The scenario says:

- **Given** SKU `book` has 3 available units and none reserved
- **When** 2 units are reserved
- **Then** the request succeeds, 1 unit remains, and one reservation event is appended

Once I or an AI implements this, how do I know it is correct? Which requirements are still hidden? We can add more tests and snapshot comparisons, and we should. With complex existing code, humans and LLMs can both miss details.

Parity lives inside the same specification and expresses the scenario as readable, executable code. The proof supplies an example input, calls the reserve action, and asserts the expected response, inventory change, and event. Its last assertion allows one known difference: the services write their event files in different directories.

proof inventory.reserve {
  example available { sku = "book", quantity = "2" }
  when reserve(sku, quantity)
  then {
    assert (result.status == 201 &&
      result.body.sku == examples.sku &&
      result.body.available == 3 &&
      result.body.reserved == 2 &&
      result.body.remaining == 1)
    assert views.inventory == {
      "added": [{"sku": "book", "available": 3, "reserved": 2, "remaining": 1}],
      "removed": [{"sku": "book", "available": 3, "reserved": 0, "remaining": 3}]
    }
    assert (views.events.added == [] &&
      views.events.removed == [] &&
      views.events.modified.size() == 1 &&
      views.events.modified[0].path == "reservations.tsv" &&
      views.events.modified[0].before.content == "" &&
      views.events.modified[0].after.content == "reserved|book|2|2|1\n")
    assert (diff.path.size() == 5 && diff.path[0] == "views" &&
      (diff.path[1] == "filesystem" || diff.path[1] == "filesystem_state") &&
      diff.path[2] == "added" && diff.path[4] == "resource" &&
      diff.legacy.endsWith("/legacy/reservations.tsv") &&
      diff.target.endsWith("/target/reservations.tsv"))
  }
}

Source

We then run Parity. It runs the legacy service first, evaluates the written assertions, and captures supported behavior automatically. It runs the Rust service with the same input and compares both observations.

$ parity verify --scenario inventory.reserve --verbose
PASS inventory.reserve [available]
  PASS (auto) views.filesystem_state: FILE_EDIT reservations.tsv
… <66 chars omitted> (legacy 1/1, target 1/1)
  PASS (auto) views.filesystem_state: FILE_EDIT project/.parity/runtime/legacy/reservations.tsv
  PASS (auto) views.postgres: POSTGRES connection:database
  PASS (auto) views.postgres_state_state: STATE_CHANGE connection:database/database/public.inventory
Summary: 1 passed, 0 failed, 0 errors, 0 skipped
Proof checked.

The output shows that the response, stock, event, database traffic, and database state match. It also shows the event-file path difference allowed by the proof.

Multiple examples and fuzzing

A small set of examples can miss bad inputs. Another scenario describes what the service should do with one:

- **Given** a reservation path contains an invalid SKU or quantity
- **When** the reservation is requested
- **Then** the request is rejected without changing inventory or appending an event

The check has four named examples and generates four more inputs. These additional cases exercise invalid SKUs and quantities without writing each one by hand.

proof inventory.invalid-reservation {
  example uppercase-sku { sku = "BOOK", quantity = "1" }
  example zero-quantity { sku = "book", quantity = "0" }
  example non-numeric-quantity { sku = "book", quantity = "two" }
  example excessive-quantity { sku = "book", quantity = "10000" }
  generate 4 cases {
    sku = text matching "[a-z]{1,12}"
    quantity = text matching "[1-9][0-9]{4}"
  }
  when reserve(sku, quantity)
  then {
    assert (result.status == 400 && result.body.error == "invalid_request")
    assert views.inventory == {"added": [], "removed": []}
    assert views.events == {"added": [], "removed": [], "modified": []}
  }
}

Source

When run, Parity verifies each named and generated case:

$ parity verify --scenario inventory.invalid-reservation --seed 0 --verbose
PASS inventory.invalid-reservation (8 cases)
  PASS uppercase-sku
  PASS zero-quantity
  PASS non-numeric-quantity
  PASS excessive-quantity
  PASS generated-1
  PASS generated-2
  PASS generated-3
  PASS generated-4
Summary: 8 passed, 0 failed, 0 errors, 0 skipped
Proof checked.

The full demo covers a reservation, bad inputs, missing stock, too little stock, and an inventory read.

Let’s break two things to see what this comparison catches.

Capture missing side-effects

A successful reservation writes a file as a side-effect. I removed that write in Rust and ran the scenario again.

$ parity verify --scenario inventory.reserve --verbose
FAIL inventory.reserve [available]
  MISMATCH views.events/modified/0: legacy and target differ at observations/reserve/effects/events/delta/modified/0
  MISMATCH (auto) views.filesystem_state FILE_EDIT project/.parity/runtime/legacy/reservations.tsv: target -{"step":"settle","phase":"settle","actor":"subject","before":{"mode":420,"uid":0,"gid":0,"links":1},"after":{"mode":420,"uid":0,"gid":0,"links":1}}
  PASS result reserve.result (1/1 cases)
  FAIL views.events (0/1 cases)
  PASS views.inventory (1/1 cases)
Summary: 0 passed, 1 failed, 0 errors, 0 skipped
Proof checked.

Source

The response and stock checks still pass. The event check fails, and automatic audit also reports that the expected file change is gone.

Detect a racing issue

The COBOL service checks the stock and reserves it in one database operation:

STRING
    "WITH updated AS ("
    "UPDATE inventory SET reserved = reserved + $2 "
    "WHERE sku = $1 AND available - reserved >= $2 "
    "RETURNING sku, available, reserved, available - reserved AS remaining"
    ") SELECT TRUE AS reserved_now, sku, available, reserved, remaining "
    "FROM updated UNION ALL "
    "SELECT FALSE AS reserved_now, sku, available, reserved, "
    "available - reserved FROM inventory "
    "WHERE sku = $1 AND NOT EXISTS (SELECT 1 FROM updated)"
    X"00"
    DELIMITED BY SIZE INTO WS-SQL-COMMAND
END-STRING

Source

PostgreSQL can accept one request and reject the other when two customers try to reserve the last item at the same time. Losing that atomic operation in the new code would introduce a serious bug.

For the experiment, I changed the Rust service to read the inventory and update it in separate queries.

let Some(current) = self.find(sku).await? else {
    return Ok(None);
};
if current.available() - current.reserved() < quantity.get() {
    return Ok(Some(ReservationOutcome::Insufficient(current)));
}

let sku = sku.as_str();
let requested = quantity.get();
let parameters: &[(&(dyn ToSql + Sync), Type)] =
    &[(&sku, Type::TEXT), (&requested, Type::INT4)];
let row = self
    .client
    .query_typed_one(UPDATE_INVENTORY, parameters)
    .await?;
let inventory = inventory_from_row(&row)?;

self.append_event(&inventory.event_line(quantity))?;
Ok(Some(ReservationOutcome::Reserved(inventory)))

Source

The request still returned 201, left one item, and wrote the event. A test that checked the response or final data would pass.

Parity failed. This is the focused part of the output:

$ parity verify --scenario inventory.reserve --verbose
FAIL inventory.reserve [available]
  PASS (auto) views.filesystem_state: FILE_EDIT reservations.tsv
  MISMATCH (auto) views.postgres POSTGRES connection:database: expected request.0.parameter_types.1=23, request.0.sql="WITH updated AS (UPDATE inventory SET reserved = reserved + $2 WHERE sku = $1 AND available - reserved >= $2 RETURNING sku, available, reserved,… <320 chars omitted>
    - request.0.parameter_types.1 = 23
    + request.0.parameter_types.1 = <none>
    request.0.sql:
      - WITH updated AS (UPDATE inventory SET reserved = reserved + $2 WHERE sku = $1 AND available - reserved >= $2 RETURNING sku, available, reserved, available - reserved AS remaining) SELECT TRUE AS reserved_now, sku, available, reserved, remaining FROM updated UNION ALL SELECT FALSE AS reserved_now, sku, available, reserved, available - reserved FROM inventory WHERE sku = $1 AND NOT EXISTS (SELECT 1 FROM updated)
      + SELECT sku, available, reserved, available - reserved AS remaining FROM inventory WHERE sku = $1
    - request.4.parameter_types.0 = <none>
    + request.4.parameter_types.0 = 25
    … 55 more changes
Summary: 0 passed, 1 failed, 0 errors, 0 skipped
Proof checked.

The response, inventory, and event checks still pass. Automatic audit reports that Rust now reads and updates in separate database requests. A reviewer can see the concurrency risk without anyone having written an assertion about the SQL shape.

How automatic audit works

Parity follows each program and the work it starts during a scenario. It observes supported process activity, network calls, files, and state without requiring either application to be changed.

Parsers turn captured traffic into operations that engineers can read. PostgreSQL traffic becomes requests, parameters, rows, and results. HTTP traffic becomes methods, paths, bodies, and responses. Parity then compares the legacy and replacement observations.

If Parity cannot parse supported traffic or capture complete evidence, required audit stops instead of returning a pass.

Automatic audit currently requires a privileged Linux runner. It covers supported process, network, filesystem, and PostgreSQL behavior. It does not cover brokers, browsers, shadow traffic, or inputs the proof did not run.

You decide what may change

Parity requires each captured value to match by default, even when the proof does not mention it. Any difference between legacy and target has to be explicit. This needs no equality boilerplate and can live inside Markdown, making the proof easier to review before and after implementation.

The Rust service uses its own modules, types, and libraries. Parity compares behavior without forcing Rust to copy the shape of the COBOL code.

Limitations

It’s important to stress that proof by observation is not the same as logical proof. Parity does not prove by itself that a target is identical to legacy. On top of that, larger systems could use CICS/DB2/VSAM to manage more involved production loads and concurrency mechanisms. Parity by itself is not meant as a stand-alone solution.

That said, the same technology we use with Parity, allows us to run slices next to production (and/or other busy environments), and effectively compare legacy to target with real data. Larger amounts of data combined with the closed behavior capture of Parity, promises a significant potential boost to migration confidence.

Parity inside Bosun

Bosun guides a migration from assessment to pull request, bit by bit. Parity checks each migration slice so reviewers can see the intent, results from both programs, automatically observed behavior, and each accepted difference.

An LLM can change the code and run the checks. Each scenario gives the reviewer evidence to decide whether the replacement did the job the team gave it.

Parity is a development preview. The checks in this article work today. We are still developing how teams use Parity across larger migrations.

If you are planning a legacy modernization and want to see what Parity finds in one of your user journeys, request a Bosun demo.