Congruent — proving AI-rewritten code equivalent (or finding the input that breaks it)

This is the spine of the whole site made literal. Coding agents refactor, migrate, and "optimize" code constantly, and the honest answer to "did that preserve behavior?" is usually tests plus vibes. Congruent gives a real answer for a deliberately narrow slice: EQUIVALENT up to bound N or COUNTEREXAMPLE: <concrete input> — with nothing hand-wavy in between.

It's hardware equivalence checking aimed at trusting AI-written code.

The problem

You can't gate a refactor on "the tests still pass" — tests only sample the input space. For a function transformation you want the stronger claim: there is no input, within a stated bound, on which these two functions disagree. That's an equivalence-checking problem, and the formal-methods toolkit answers it properly.

Approach — cheap checks first, proof only when needed

The escalation ladder is the design:

1. Differential testing — property-based random + boundary inputs kills obvious non-equivalence in milliseconds. A counterexample here ends the run.
2. Symbolic execution → SMT — lower both functions' bounded behavior to Z3 bit-vector constraints, assert inputs equal ∧ outputs differ, and solve. UNSAT means equivalent within bound; SAT decodes back to a concrete counterexample.
3. Bounded model checking — unroll loops/recursion to depth k and report the bound honestly.

Why it's trustworthy — the part that matters

The credibility is the honesty about limits:

• A real UNKNOWN verdict. When the symbolic stage declines to model something, the result is UNKNOWN — never silently upgraded to EQUIVALENT.
• Every verdict carries its bound and assumptions (integer width, unroll depth, preconditions). No unconditional soundness is ever claimed.
• A soundness gate in CI. bench_recall.py exits non-zero on any unsound verdict (a false EQUIVALENT or false COUNTEREXAMPLE) — currently 10/10 fixtures decided, 0 unsound.

The demo it's built to land

An LLM "simplifies" lo + (hi - lo) // 2 to (lo + hi) // 2. Congruent catches the 32-bit overflow with the exact inputs (lo=1, hi=2147483647), and proves honest rewrites correct — distributivity over modular arithmetic — via Z3 in milliseconds. One screenshot of proof-or-counterexample on a real AI refactor communicates the whole value.

Status & what's next

Core complete: a Python subset with ints/bools, branches, bounded loops, assume(...) preconditions, and bounded list[int] — plus a C subset front end, so the same engine decides rewrites in a second language. Out of scope for v1 (and on the roadmap): floats, side effects, heap aliasing, unbounded loops.