2026-11-02 upgrade

We tried to make it lie, and it did, four ways. All four are fixed, and the fuzzer that found the biggest one now runs as a test.

1. Division by zero. return 10 // x was "proved for all inputs" though it raises at x = 0; 70 of 250 fuzzed proofs were like this. Now every // and % in the function, precondition and postcondition carries a non-zero obligation, following Python's short-circuit order, and a violation is a counterexample with its failure kind.
2. Shadowed built-ins. abs = lambda v: -1 next to the function made Z3 "prove" result >= 0. Module-level code, decorators, and parameters or locals named abs/min/max are now refused.
3. Engine crash. if x: on an int raised inside the engine. Now refused with a clear reason.
4. Docstrings. A function with a docstring was refused. Now accepted, and the offline re-checker accepts it too.
5. Certificates. Carry the failure kind; recheck.py reproduces "raises" counterexamples by confirming Python raises there.

Measured: 1,500 fuzzed contracts before (70 false proofs, 645 mislabelled counterexamples); 3,000 after, on two seeds, with 0 wrong verdicts. 18 new tests, 46 VeriCoding tests in all passing.

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.