congruent-eq 0.0.1

Prove behavioral equivalence between an original function and an AI-rewritten one within bounds, or return the concrete input that breaks it.

Congruent

Given an original function and an AI-rewritten one, prove behavioral equivalence within bounds, return the concrete input that breaks it — or admit it doesn't know.

Coding agents refactor, migrate, and "optimize" code constantly. The honest answer to "did this preserve behavior?" is usually tests plus vibes. Congruent gives a real answer for a deliberately narrow slice of the problem: EQUIVALENT up to bound N, COUNTEREXAMPLE: <concrete input>, or an honest UNKNOWN — never a guess dressed up as a proof.

It's equivalence checking (the EDA/formal-methods kind) pointed at the problem of trusting AI-generated code.

---

Scope (read this first)

The credibility of this tool is its honesty about what it does and doesn't do. v1 is intentionally small.

In scope (v1)	Out of scope (v1 — see ROADMAP.md)
Pure, deterministic functions (no I/O, no global mutation)	Side effects, I/O, concurrency
Bounded inputs: machine ints, bools, fixed-length lists, bounded strings	Floating-point exactness
Integer/boolean arithmetic, comparisons, branches	Recursion / function calls; unbounded loops (loops are bounded, unrolled to depth k)
Bounded loops (return/break/continue), unrolled to depth k	Heap aliasing, full object semantics
A Python subset, plus a C subset front end	Full language semantics

Verdicts:

• EQUIVALENT up to bound N — no diverging input exists within the bound (proven by the symbolic stage; for the current loop-free subset this is complete over all inputs at the chosen width).
• COUNTEREXAMPLE: <input> — a concrete input where the two functions disagree, with both outputs.
• UNKNOWN — no counterexample found, but equivalence not proven (e.g. the symbolic stage declined to model something — see below). Never silently upgraded to EQUIVALENT.

Congruent never claims unconditional soundness. Every verdict carries its bound and assumptions.

---

How it works

Cheap checks first, expensive proof only when needed:

1. Differential testing (difftest.py) — property-based random + boundary inputs. Kills obvious non-equivalence in milliseconds. A counterexample here ends the run.
2. Symbolic execution → SMT (symbolic.py + solver.py) — translate both functions' bounded behavior into logical constraints, assert inputs equal ∧ outputs differ, and ask Z3. UNSAT = equivalent within bound; SAT = the model decodes back to a concrete counterexample.
3. Bounded model checking — unroll loops to depth k, verify up to that bound, report the bound. (Recursion / function calls are out of scope.)

input: fn_original, fn_candidate (source) + bound config
  ├─ parse → normalized typed IR        (ir.py)
  ├─ Stage 1: differential tester ──► counterexample? ─► REPORT   (difftest.py)
  ├─ Stage 2: symbolic engine                                     (symbolic.py)
  │     • symbolically execute each fn over fresh symbolic inputs
  │     • collect path constraints + output expressions
  │     • build (inputs equal) ∧ (outputs differ) → Z3 solve      (solver.py)
  │           • UNSAT → EQUIVALENT up to bound N
  │           • SAT   → decode model → COUNTEREXAMPLE
  └─ REPORT (verdict, bound, counterexample, solver stats, caveats)  (report.py)

---

The demo it's built to land

An LLM "simplifies" a midpoint calculation:

# original (correct under fixed-width ints)
def mid(lo: int, hi: int) -> int:
    return lo + (hi - lo) // 2

# candidate (AI "simplification")
def mid(lo: int, hi: int) -> int:
    return (lo + hi) // 2

Congruent catches it:

$ congruent original.py:mid candidate.py:mid --bound 8 --int-width 32
COUNTEREXAMPLE  (stage: difftest)
  inputs:    lo = 1, hi = 2147483647
  original:  1073741824
  candidate: -1073741824        # 32-bit overflow in (lo + hi)
  note: 32-bit two's-complement integers

And it proves the honest rewrites correct — distributivity over modular arithmetic, here, via Z3:

$ congruent original.py:f candidate.py:g          # (x+y)*2  vs  x*2 + y*2
EQUIVALENT  (stage: symbolic, 0.00s)
  equivalent (complete — no bound needed)
  note: 32-bit two's-complement integers
  note: complete: agree on all 32-bit inputs (no loops to bound)

Note what that verdict does not say: there is no loop and no list here, so the bound never binds — the pair is decided over the entire 32-bit input space. A result that genuinely is complete says so, rather than hiding behind a bound.

One screenshot of proof-or-counterexample on a real AI refactor communicates the whole value.

It also handles bounded loops. A reversed-accumulation refactor is proven equivalent up to the unroll bound:

$ congruent original.py:f candidate.py:g --bound 8   # sum i  vs  sum (n-1-i)
EQUIVALENT  (stage: symbolic, 0.01s)
  equivalent up to bound 8
  note: 32-bit two's-complement integers
  note: holds within bound: loops up to 8 iterations

And you can scope the question with a precondition — equivalence often only holds on part of the input domain:

$ congruent ident.py:f abs.py:g                  # x  vs  (x if x>=0 else -x)
COUNTEREXAMPLE  (stage: difftest)
  inputs: x = -1                                 # they disagree on negatives
$ congruent ident.py:f abs.py:g --assume 'x >= 0'
EQUIVALENT  (stage: symbolic, 0.00s)
  note: precondition: x >= 0

Declare a precondition inline with a leading assume(...) in the reference function, or pass --assume on the CLI.

And it reasons about list[int] inputs — here it proves a hand-written count equals len, for every list up to the length bound:

$ congruent original.py:f candidate.py:g          # len(xs)  vs  count loop
EQUIVALENT  (stage: symbolic, 0.00s)
  note: holds within bound: lists/strings up to length 8, loops up to 8 iterations

Status: M0–M7 complete, plus the LLM closed-loop stretch. The differential stage catches counterexamples (overflow included) under a fixed-width integer model; the symbolic stage lowers both functions to Z3 bitvector expressions and returns EQUIVALENT (UNSAT), a COUNTEREXAMPLE (SAT, decoded to concrete inputs), or UNKNOWN. Supported: ints/bools, branches, for ... in range(...) and for x in xs loops (bounded model checking) with return/break/continue, assume(...) preconditions, and bounded list[int] both as inputs (len, iteration, xs[i]) and as outputs (build and return a list via literals + +), and bounded str (literals, len, ==, +, indexing incl. Python negative indices, iteration). Out-of-bounds access and divide-by-zero are modeled as runtime errors (a rewrite that crashes where the original didn't is a counterexample); falling off the end without returning yields Python's None — a value distinct from both a raised exception and any returned value. Counterexamples are minimized to the smallest failing input. An optional --cross-check re-decides each query with CVC5. Benchmarks pass with zero unsound verdicts. See PROGRESS.md and ROADMAP.md.

---

Install

Congruent is distributed on PyPI as congruent-eq; you still import congruent and run the congruent CLI.

pip install congruent-eq

Or from source:

git clone <repo-url> congruent
cd congruent
python -m pip install -e ".[dev]"

Requires Python 3.11+. The solver backend is z3-solver.

Usage

congruent path/to/original.py:func_name path/to/candidate.py:func_name --bound 8

Flag	Default	Meaning
--bound N	8	Loop unroll depth and list/string-length bound
--int-width W	32	Bit width for the fixed-width integer model
--assume EXPR	—	Precondition on the inputs, e.g. --assume 'n >= 0' (repeatable)
--no-minimize	off	Report the first counterexample found, not the smallest
--cross-check	off	Re-decide with CVC5 and flag any disagreement (needs pip install "congruent-eq[cross-check]")
--timeout S	300	Give up on the solver after S seconds and report UNKNOWN (0 = no limit)

Some queries are genuinely intractable — multiplying unknowns by unknowns in a loop (a polynomial with symbolic coefficients) is the classic one. --timeout bounds them: the verdict degrades to an honest UNKNOWN, never a hang and never a false EQUIVALENT. See benchmarks/README.md.

Layout

src/congruent/
  ir.py         # Python AST → normalized typed IR
  cfront.py     # C front end (pycparser → the same IR)
  difftest.py   # differential prefilter + fixed-width concrete interpreter (Stage 1)
  symbolic.py   # symbolic interpreter → Z3 exprs (Stage 2)
  solver.py     # equivalence query, model decoding, minimization
  backends.py   # CVC5 cross-check (independent second opinion)
  equiv.py      # orchestration, escalation, Verdict data model
  report.py     # verdict formatting
  refine.py     # the LLM closed loop (AI proposes → Congruent verifies → feedback)
  cli.py        # `congruent a.py:f b.py:g --bound 8`
tests/          # 229 tests incl. fuzz + oracle soundness guards
examples/       # gallery of realistic AI-refactor pairs (Python + C), runner,
                #   closed_loop_demo.py (offline/--live), live_rewrite.py (your code)
benchmarks/     # recall gate, timing-vs-bound, self-validating fuzzer,
                #   realpy_fuzz.py (semantics oracle), numpy_oracle.py (wrapping oracle)
docs/demo.svg   # the README demo image
docs/live_run.md # captured live-model sessions (caught, corrected, proven)

Gallery

examples/ holds realistic AI-refactor pairs — faithful rewrites and subtly broken ones — with Congruent's verdict on each (binary-search midpoint, clamping, list maximum, sum-to-n, counting). The largest entry, water_bill.py, is a ~50-line tiered-billing routine whose candidate was written by a live model and accepted only after proof; a second, polyval.py, is numpy's own Horner loop seed-optimized by a live model — both captured in docs/live_run.md. Run them all:

python examples/run_gallery.py

Closed loop: AI proposes, Congruent verifies

The stretch feature (refine.py) closes the loop: an LLM proposes a rewrite, Congruent checks it, and any counterexample is fed back so the model can fix its own mistake — repeating until the rewrite is proven equivalent within the bound. The loop never accepts an unverified rewrite.

python examples/closed_loop_demo.py          # offline, deterministic (a scripted LLM)
python examples/closed_loop_demo.py --live   # a real model via the Anthropic API
python examples/live_rewrite.py FILE.py:func # point the live loop at your own code

The demo shows Congruent catching a plausible-but-wrong refactor and guiding the fix — e.g. an agent "simplifies" a midpoint to (a + b) // 2, Congruent returns the exact overflowing input, and the next attempt reverts to the safe form and is proven equivalent. This is not hypothetical: in a live run, a real model (claude-opus-4-8) made exactly that mistake, was handed the overflowing input, and came back with the proven-safe form — the unedited transcript is in docs/live_run.md. The rewriter is pluggable via a Rewriter protocol: ScriptedRewriter (offline, used by the demo and tests) or AnthropicRewriter (pip install "congruent-eq[llm]", reads ANTHROPIC_API_KEY).

Benchmarks

python benchmarks/bench_recall.py     # verdict vs. expectation over the eval set
python benchmarks/bench_scaling.py    # solver time vs. --bound
python benchmarks/fuzz.py             # random pairs, each verdict re-checked
python benchmarks/realpy_fuzz.py      # interpreter vs. real Python (semantics oracle)
python benchmarks/numpy_oracle.py     # wrapping vs. numpy fixed-width ints (overflow oracle)

numpy_oracle.py needs the oracle extra: pip install "congruent-eq[oracle]" (from source: python -m pip install -e ".[dev,oracle]"). Everything else in that block runs on the core install.

bench_recall.py exits non-zero if any verdict is unsound (a false EQUIVALENT or false COUNTEREXAMPLE), so it doubles as a soundness gate. fuzz.py is the deepest check: it generates random function pairs, asks Congruent, and then independently re-validates each verdict against the concrete interpreter — so a false verdict fails loudly. It re-verifies clean on the current code (3,000 random pairs, 0 unsound, at its default settings), and tens of thousands more passed across seven adversarial audit rounds (plus Z3↔CVC5 cross-checks); a small deterministic batch runs in the test suite.

Two more oracles validate the interpreter every other check trusts, each against a reference that shares no code with Congruent — one per half of the fixed-width model. realpy_fuzz.py unparses generated IR back to real Python and diffs the behavior (this caught the negative-indexing bug both stages shared); it runs wide so nothing overflows, isolating semantics. numpy_oracle.py covers the other half — the two's-complement wrapping itself — by re-evaluating random integer functions with numpy's C fixed-width scalars at small widths where overflow is the common case; it agrees with the interpreter across 8/16/32/64 (and matches Congruent's arithmetic exhaustively over every 8-bit operand pair, overflow edges included). Both run a deterministic slice in the test suite.

The measured operating envelope — solver time out to bound 1024, where the cliff is, and why the default bound is 8 — is documented in benchmarks/README.md.

Roadmap & progress

• ROADMAP.md — milestones M0→M7 and the out-of-scope list as future work.
• PROGRESS.md — current state, M0 checklist, and open design decisions.

License

MIT — see LICENSE.