Behavioral verification

Agents write. Strust verifies.

Strust runs existing software and its AI-written replacement together, then retains the first changed behavior as replayable evidence.

Inspect the demoRead research
paired executionclaims / F-02
Existing behaviorSKIP_WRITEBlank account ID
Replacement behaviorWRITE_FALLBACKNull-only guard
First changed decisionBranch action
VerdictDIVERGEBlank account took a new write path
Same record. The verifier keeps the first changed branch for the agent and reviewer.
ReferenceExisting executable
CandidateAI-written replacement
VerdictMATCH / DIVERGE / INCONCLUSIVE
First laneCOBOL to Java

The contract stays fixed while the code changes.

Strust runs existing software and its AI-written replacement against one approved behavioral boundary.

  1. Verifier

    Pin the contract

    Approve the reference, inputs, runtime assumptions, observations, and comparison policy.

  2. Runner

    Execute the pair

    Run the existing system and candidate rewrite under the same declared conditions.

  3. Comparator

    Find the origin

    Stop at the earliest contract-relevant difference, before downstream effects obscure it.

  4. Evidence store

    Retain the evidence

    Return a replayable finding to the coding agent and a reviewable decision to the owner.

One changed decision. Two useful views.

Agent view isolates the next patch. Reviewer view translates the evidence into impact and a human decision.

This controlled example illustrates the intended loop; the paper states which arithmetic is reproducible and which historical execution artifacts are unavailable.

COBOL to Java

Agent receives

Trace-local cause, the first divergent decision, a suggested patch, and a conceptual replay target.

Agent diagnosis / F-02

1 changed observation

First divergence: Branch action

Batch branch B-17 / null-account path / Illustrative scenario B

Cause isolated. Patch the changed branch and rerun.

Reference system

COBOL

IF ACCOUNT-ID = SPACES

NEXT SENTENCE

ELSE PERFORM WRITE-CLAIM

END-IF

Candidate system

Java

if (accountId == null) {

writeFallback(claim);

} else { writeClaim(claim); }

batch.advance();

Execution checkpoints

Source value / target value

  1. NULL

    Account input

    NULL

    Equivalent

  2. TRUE

    Guard B-17

    TRUE

    Equivalent

  3. SKIP_WRITE

    Branch action

    WRITE_FALLBACK

    Origin

  4. 0

    Rows emitted

    1

    Changed

  5. UNCHANGED

    Batch count

    INCREMENTED

    Changed

First divergence

The first changed decision is Branch action: the source returns SKIP_WRITE while Java calls writeFallback.

Capture → Compare → Isolate → Patch → Rerun

Compilation can pass while behavior moves.

COBOL is the first executable reference. Fixed-width data and runtime assumptions make it an unforgiving test lane.

Observed sourceCOBOL
CUSTOMER-CODE PIC X(8).

IF CUSTOMER-CODE = 'VIP'
  MOVE 'PRIORITY' TO QUEUE-NAME
Candidate rewriteJava
String code = record.customerCode();
if (code.equals("VIP")) {
  queueName = "PRIORITY";
}

Open evaluation protocol

A benchmark for behavior, not syntax.

SemaMig-Bench runs held-out workloads against the executable source and native Java candidate. Contract-relevant observations agree, or the task does not pass.

Read benchmark PDF
Task unit
Paired execution

COBOL reference and native Java candidate

Pass condition
Behavioral agreement

Declared observations match under the contract

Evidence
Reviewable finding

Per-task verdict, comparison output, and failure context

Bring the rewrite you cannot afford to get wrong.

Tell us what is changing and what behavior must stay the same.

Contact Strust