Behavioral verification for AI-written software

Prove an AI migration didn't change what your software does.

Strust runs the legacy system and its AI-written replacement on the same inputs, pinpoints the first behavior that diverged, and hands the evidence to both the coding agent and human reviewer. Starting with COBOL-to-Java.

Become a design partner See the interactive demo

Stage

V1 demonstrator

Evidence

10 controlled scenarios

Benchmark

V1 protocol published

Status

Seeking design partners

Interactive v1 demonstrator

Agent + reviewer views

One change. The agent fixes it; the reviewer decides it.

Agent view isolates the first changed decision and the next patch. Reviewer view translates that evidence into impact and a human decision. This controlled example illustrates the intended product loop; the published paper documents the current evidence and limits.

COBOL to Java

Agent receives

Trace-local cause, the first divergent decision, a suggested patch, and the exact rerun command.

Agent diagnosis / F-02

12 divergent traces

First divergence: Branch action

Batch branch B-17 / null-account path · Trace 417 / 1,215

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

NULL
Account input
NULL
Equivalent
TRUE
Guard B-17
TRUE
Equivalent
SKIP_WRITE
Branch action
WRITE_FALLBACK
Origin
0
Rows emitted
1
Changed
4,808
Batch count
4,809
Changed

First divergence

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

Capture → Compare → Isolate → Patch → Rerun

Use the lightest check that can answer the question.

Change criticality

Selected feedback

Add replay and broader input coverage.

4/ 5

Types + static analysis
Global invariants
Immediate
Expect-style examples
Readable behavior
Milliseconds
Deterministic replay
Controlled time + effects
Seconds
Property + fuzz checks
Input exploration
Selective
Historical + formal checks
Highest assurance
Critical paths

Evaluator firewall

The agent does not grade itself.

Strust separates implementation changes, eval changes, and new expected behavior. If a patch changes both the code and the rule judging it, that decision is surfaced for human review.

Implementation diffEval diffHuman approval

An eval is a readable example of intent.

.strust/evals/null-account-output.evalRepository eval case

case "null account emits no row"

risk critical
input account_id = null
expect rows = 0
expect effects = []
owner payments-platform

Text first

The test is also the explanation.

Each case records why the behavior matters, the controlled input, expected outputs and side effects, its owner, and its criticality. Humans can read it. Agents can act on it.

Survives after the reference system is retired

CLI

strust eval --changed

Agent tool

Focused failure context

Risk-sensitive gates

Pull request

Behavioral diff

Migration was the first proving ground.

First product laneCOBOL → Java

COBOL — observed

01 CUSTOMER-CODE PIC X(8).

IF CUSTOMER-CODE = 'VIP'
  MOVE 'PRIORITY' TO QUEUE-NAME

Java — converted

String code = record.customerCode();
if (code.equals("VIP")) { // ← flagged
  queueName = "PRIORITY";
}

A legacy system is already an executable reference. Strust turns representative source behavior into evals for the system replacing it. Here, COBOL pads the shorter fixed-width value; Java treats VIP····· and VIP as different strings. Both compile; the behavior changes.

✓Capture the source system as executable behavior

✓Review each source-to-target divergence

✓Keep approved cases for every later change

Read the original migration research

A benchmark for whether migration agents preserve behavior.

SemaMig-Bench · Benchmark v1

Run the source. Run the migration. Score the behavior.

SemaMig-Bench turns COBOL-to-Java migration into a paired, held-out evaluation. The same workload runs against the executable source and native Java candidate; a task passes only when the contract-relevant observations agree.

Explore SemaMig-Bench Open benchmark paper

Protocol

Published

Five-page design and preregistered evaluation protocol

Task corpus

In construction

50 tasks planned across diagnostic, workflow, and system tiers

Leaderboard

Results forthcoming

Baseline scores publish after the v1 corpus and verifiers are frozen

Seeking design partners

Bring one real migration into the loop.

Strust is looking for engineering teams, modernization firms, and coding-agent builders with an important software change to verify. Bring the workflow; we will map the behavior that matters and show where the candidate diverges.

1.Define the behaviors and side effects that matter

2.Run the reference and candidate under one contract

3.Review retained evidence and the first divergence

Prefer email? [email protected]

Tell us about the change

Start with the workflow, not a sales call.

Share enough context for us to decide whether the current demonstrator and research can support a useful first pass.