Lockstep

Translation is a commodity. Proof is the product.

Lockstep is an independent verifier for code migration. It does not translate code and it does not analyze source. It witnesses behavior: it runs the legacy program and its replacement against the same inputs and observes them at the boundary where the outside world can tell them apart. The output is a deterministic, replayable, tamper-evident behavioral equivalence certificate: what was proven identical, under which explicit assumptions, and, printed just as large, what was not.

Why this exists

AI can now translate legacy code (COBOL, and the rest of the spine the world quietly runs on) into modern languages at scale. Translation tools advertise things like "80% accuracy." Eighty percent accurate on a payment system means twenty percent unverified-wrong, and nothing in the toolchain measures which twenty percent. Lockstep is that measurement: an execution-based check that the migrated system does the same thing as the original, with the evidence written down and checkable by anyone.

Design principles

1. Execution is ground truth. For questions of behavioral trust, the inside of a program is the wrong place to look; source-level reasoning is expensive, language-bound, and convinces engineers rather than auditors. Lockstep contains no parser, no code graph, no static analysis of the systems under test. Programs are black boxes observed at their boundary.
2. Behavior at the observable boundary is the program's identity. Two systems indistinguishable under every observation are, for every practical purpose, the same system.
3. Total equivalence is undecidable (Rice's theorem). Anyone claiming certainty is wrong. The honest claim, and the only defensible one, is bounded evidence: equivalence demonstrated on an explicit input corpus, under an explicit assumption ledger, with every unverified surface named. The impossibility result is the reason the output is honest by construction, not a weakness to hide.
4. The certificate verifies itself. Deterministic replay, hash-chained trials, byte-stable output. Trust the instrument, not the operator.

What it does

lockstep attest <spec.json>     run legacy vs candidate over the corpus,
                               emit certificate.json + certificate.md;
                               --sign SEEDFILE embeds an Ed25519 signature
lockstep check <certificate>    verify a certificate's internal integrity
                               (hash chain, counts, verdict consistency)
                               and, if signed, its authenticity;
                               --pubkey HEX pins the expected signer
lockstep replay <spec> <cert>   re-run the trials and confirm the certificate
                               still holds on this machine, byte for byte
                               (signature fields excluded: content must
                               reproduce, the signature depends on the key)

• Spec: the two commands under test, the input corpus, the observable boundary (stdout / stderr / exit code / declared output files), and the assumption ledger: env pinning, float tolerance, line-order normalization, timestamp masking. Every leniency granted is declared.
• Trial: one input, both systems, observations captured and normalized per the ledger, compared, hashed.
• Certificate: the verdict per trial and overall, one of EQUIVALENT, DIVERGENT, or REFUSED (nondeterminism, timeout, or unobservable surface). A hash chain across trials means no trial can be silently dropped or reordered, and the spec + ledger are embedded by hash.

Divergence is a finding, not a failure: it is either a defect in the migration or load-bearing legacy behavior the rewrite missed. Both are exactly what you ran the check to learn.

Quickstart

demo/payroll/ migrates a Python payroll job to Rust. The faithful port certifies EQUIVALENT; a version that swaps exact-decimal rounding for naive binary float is caught DIVERGENT at a single half-cent, with the input, line, and both values named in the certificate. demo/cobol-interest/ does the same against a real GnuCOBOL program.

cargo build --all-targets
./target/debug/lockstep attest demo/payroll/spec-correct.json -o out   # EQUIVALENT (exit 0)
./target/debug/lockstep attest demo/payroll/spec-buggy.json   -o out   # DIVERGENT  (exit 2)
./target/debug/lockstep check out/payroll-py-to-rust.certificate.json  # INTACT

Signing certificates

A keyless certificate proves consistency, not authenticity: anyone who reads the (fully documented) hash construction can fabricate a passing document. To bind a certificate to a known authority, sign it at attestation time with an Ed25519 seed:

head -c 32 /dev/urandom > attestor.seed          # the seed IS the signing key
./target/debug/lockstep attest spec.json --sign attestor.seed -o out
./target/debug/lockstep check out/name.certificate.json
#   SIGNED (authentic), with the signer's public key printed
./target/debug/lockstep check out/name.certificate.json --pubkey <hex>
#   additionally requires the embedded key to be the one you already trust

The seed file holds either exactly 32 raw bytes or 64 hex characters. Signing adds two fields, public_key and signature. The public key is bound into certificate_sha256 (the hash is computed with the key present and the signature blanked), so an attacker cannot swap in their own key without breaking the hash; the signature then covers that hash. Auditors should run check --pubkey <hex> so that only certificates signed by a key they already trust are accepted. Unsigned certificates verify exactly as before, and check labels them UNSIGNED so nobody mistakes integrity for authenticity. replay compares certificate content with the two signing fields excluded, so replay works identically for signed and unsigned certificates.

Engineering principles

• Rust, std-only, zero external dependencies. The supply chain is an attack surface, and the whole instrument should be readable end to end.
• #![forbid(unsafe_code)].
• Deterministic and byte-stable: same spec + same corpus + same binaries → identical certificate, hash for hash.
• The verifier is smaller than the claim: check is auditable in one sitting.
• Refuse-and-flag over guess-and-hope, everywhere.

Status & non-goals

v0. Batch programs (stdin → stdout/exit/files), the shape of most legacy jobs. Not yet: service/traffic replay, interactive sessions, or general concurrency (these are REFUSED and named, never silently passed).

lockstep check proves a certificate's internal consistency and, for signed certificates, its authenticity: attest --sign embeds an Ed25519 public key and a signature over the certificate hash, and check --pubkey pins the certificate to a signer you already trust. This closes finding C1 of docs/AUDIT-v0.md for signed certificates. An unsigned certificate remains forgeable by construction; check reports it UNSIGNED so the two claims are never confused.

Honest caveat: the SHA-512 and Ed25519 in src/sign.rs are implemented from scratch to keep the zero-dependency rule. They pass the RFC 8032 test vectors, but the code has not been audited by cryptographers and is not constant-time; treat it accordingly, and keep seed files offline.

Not goals, by design: no translation, no code repair, no source analysis of targets; no network, no cloud, no telemetry (airgap-clean by construction).

---

Lockstep: two systems run side by side, in step, held to the same behavior.