Evidence

A differential fuzzer: random functions and contracts inside the subset, every verdict checked by running the real Python on every input in [-5, 5] for each parameter. Our own testing, not independent.

Before the fix (seed 1, 1,500 contracts)

Outcome	Count
`COUNTEREXAMPLE_OK`	605
`CRASH_COUNTEREXAMPLE`	645
`PROVED_BUT_CRASHES`	70
`PROVED_OK`	180

PROVED_BUT_CRASHES: Z3 said "proved for all inputs" and Python raised ZeroDivisionError on one. CRASH_COUNTEREXAMPLE: the counterexample made Python raise, but was described as an ordinary violation.

After the fix

Outcome (seed 1)	Count
`COUNTEREXAMPLE_OK`	251
`PROVED_OK`	146
`RAISES_COUNTEREXAMPLE_OK`	1103

Outcome (seed 7, fresh cases)	Count
`COUNTEREXAMPLE_OK`	290
`PROVED_OK`	135
`RAISES_COUNTEREXAMPLE_OK`	1075

Every verdict correct: proofs hold on every grid input, every counterexample breaks the postcondition in Python, and every "raises" counterexample raises in exactly the part it names. The fuzzer would report FALSE_PROVED, FALSE_COUNTEREXAMPLE, PROVED_BUT_CRASHES, WRONG_FAILURE_KIND or ENGINE_ERROR; none occurred.

Hand-written probes

Case	Before	After
module-level abs = lambda v: -1, contract result >= 0	PROVED (false: returns -1)	REFUSED
parameter named abs	PROVED (false: TypeError)	REFUSED
local max = 3	PROVED (false: TypeError)	REFUSED
@staticmethod decorator	accepted (decorators ignored)	REFUSED
return 10 // x, any postcondition	PROVED for all inputs (false: raises at x=0)	counterexample x=0, function_raises
postcondition result // x == 1 or x == 0	PROVED (false: raises at x=0)	counterexample x=0, postcondition_raises
precondition 10 // x > 0	PROVED	counterexample x=0, precondition_raises
x == 0 or result // x == 1 (short-circuit)	PROVED	PROVED (correct)
if x: on an int	engine exception (HTTP 500)	REFUSED: mixes int and bool
function with a docstring	REFUSED (unsupported statement)	PROVED; certificate re-checks offline

Tests

tests/test_vericoding_soundness_2026_11_02.py 18 + test_vericoding_keystone_routes/scan 19 passed; vericoding-gate/test_vericoding_gate.py 9 passed.

Files

vericoding-evolution-2026-11-02.json	`d13400a61211d91ab15ad4c696c31717121243a6d8ef55fd0f5f1517a299a044`
vericoding-fuzz-soundness.py (the fuzzer; it needs the engine to run, so it is published to be read)	`b0cb60716461684a73a741e1648eff4eab239f8178247b4e6b701eeb5216f21c`

FIRME AI CORPORATION · CAIN-42 is a Byzantine trust fabric. Numbers marked "our own check" were run by us, not by an independent party. Nothing on these pages is a certification.