Vibe Check.

The trust check for AI-written code.

Testing says yes. The checker says forever — or hands you the counterexample.

“Forever” means all inputs in the stated mathematical model—not every program, compiler or real-world behavior. These are curated snippets, not AI-extracted specifications.

01Here’s the code

CURATED / SIGNED 32-BIT

// i32 wrapping negation (two’s complement)
function abs32(x) {
  return x < 0 ? wrapping_neg(x) : x;
}

Fidelity boundary. Exact wrapping i32 model. Not JavaScript Math.abs; Rust checked/debug negation may panic instead of wrap.

Inspect the exact SMT2 / negated property

(set-logic QF_BV)
(declare-const x (_ BitVec 32))
(define-fun result () (_ BitVec 32) (ite (bvslt x (_ bv0 32)) (bvneg x) x))
(assert (bvslt result (_ bv0 32)))

Ordinary tests / computed locally

x=-100PASS

x=-1PASS

x=0PASS

x=1PASS

x=100PASS

A handful of passing examples covers a tiny fraction of this domain—approximately 0%, not a guarantee. No test-coverage benchmark is claimed.

02The stated property

For every signed 32-bit x: abs32(x) ≥ 0.

All 2³² signed 32-bit bit patterns, including INT_MIN.

Z3 searches for an input that violates the property. SAT gives a real model; UNSAT proves no violating input exists in this encoding. Unknown or errors never count as proof.

03Run the check

Runs locally in your browser. The first run loads the solver.

04 / THE CERTIFICATE TRAVELS

Seal the evidence. Re-check the claim.

A SHA-256 integrity seal binds the code, stated property, domain, fidelity caveats, actual solver version and embedded SMT2. It is not a signature or authenticated origin. An imported “machine-proved” grade remains an assertion until a fresh re-check succeeds.

CERTIFICATE JSON / editable re-check input

Advanced: paste your own function EXPERIMENTAL PREVIEW

Coming soon. No snippet-to-property AI adapter is connected to this demo, so paste mode is disabled. AI-proposed properties may not faithfully capture your code—this is exactly the gap we gate against.