Why "1 passed in 0.01s" is a lie when AI writes the tests (and how I built a Z3 + Zig 0.17 truth gate to stop it)

Why "1 passed in 0.01s" is a lie when AI writes the tests

(and how I built a Z3 + Zig 0.17 truth gate to stop it)

• Repository: https://github.com/newmathphys/kern
• License: PolyForm Noncommercial 1.0.0 / Commercial (source-available)
• Static binary: kernc-x86_64-linux-musl in the release assets (no Zig install needed)

---

The lie is not in pytest

Let me be precise, because the title is deliberately blunt. pytest does not lie.
It reports what happened: the test function ran to completion without raising.
That is all 1 passed in 0.01s ever meant.

The lie is in the inference. When an AI agent writes both the fix and the test,
"1 passed" is presented as evidence that the fix is correct. It is not evidence of
anything, because the test was never able to fail.

Here is the actual demo from this repo (make run-example), a withdrawal function
where the agent dropped the amount <= 0 guard:

[1] pytest:  1 passed in 0.01s              <- green. The bug ships.
[2] KERN:    contract_refuted.smt2: SAT  -> e=0 (F)  COUNTEREXAMPLE
             contract_fixed.smt2:   UNSAT -> e=1 (T)  PROVED

The test contained no assert at all. It called the function and checked that no
exception was raised. An agent optimising for a green checkmark will write exactly
that, and it will keep writing it, because nothing in a boolean CI pipeline
distinguishes 1 passed (a real test) from 1 passed (an empty one).

What I built instead

KERN is an L0–L5 verification gateway written in Zig 0.17. A claim does not become
e = 1 because a test printed green. It becomes e = 1 only when an external
trusted checker (Z3) proves it, or when a reproducible execution record backs it.

Three mechanisms do the work.

1. Belnap B₄ accumulator. Verdicts are not overwritten, they are accumulated:
(p, n) -> N | T | F | B. A passing test (T) joined with a counterexample (F)
yields B — conflict. The conflict is never resolved in favour of the proof. This
is JOIN_K(T, F) = B, and it is proved in Lean 4, not asserted in a comment.

2. Can-fail harness (tools/canfail.py). Every check in the repository must
prove that it is capable of failing: the harness injects a fault and requires a
non-zero exit code. Current state:

total make targets:  89
CHECK targets:       68   (must be able to fail)
CHECK with proof of "can fail":  64/68
registered fault-injection cases: 73

This is the part that found the real problems. Auditing my own suite turned up
26 defects of a single class: "silently broken checks" — scripts or tests that
returned exit code 0 while the check itself was broken. Examples:

• ./formal/check.sh | tail -3 without pipefail — the pipeline reported the status of tail, so a failing proof check looked green;
• kernc cat image /raw/missing printed data to stderr and exited 0, so kernc cat ... > out.txt produced an empty file and no error;
• a .gitignore rule *.log placed after !docs/evidence/*.log silently excluded every verification log — the repo published claims without evidence.

3. Independent proof-DAG checker (src/verifier/proof_check.zig). Z3's unsat
is not taken on faith. KERN parses the solver's proof DAG and re-derives:

• no proof holes (hole / trust / sorry → immediate rejection);
• premise binding — every nested (asserted ...) must match a clause of the input contract (premises_unbound == 0);
• mp, unit-resolution, refl/symm/trans, and-elim, not-or-elim, monotonicity;
• Farkas arithmetic certificates for linear integer inequalities — including the ¬(l ≤ r) ⟺ r − l + 1 ≤ 0 normalisation over ℤ (where most hand-written checkers silently get the sign or the +1 wrong);
• the DAG must conclude false.

On the reference proof this now reports trusted: 0 — every one of the 16
steps is independently re-derived:

[PROOF VERIFIED] steps: 16 | premises bound: 1/1 | mp: 2 | rewrite (linear): 5 |
                 farkas: 1 | trusted: 0 | holes: 0

Honest limits (this is the part most write-ups skip)

I would rather publish the boundaries than have someone find them:

• The static gate does not raise pass@1. Measured on HumanEval+ with a real model: 0.524 base / 0.500 plus. The gate's precision is 100 % (55/55 blocks were genuine failures, 0 false blocks), but it fires before the tests, so the score is unchanged. Raising it requires execution evidence and iterative repair, not one-shot filtering.
• zstd is declared in the format and NOT implemented. Zig's std ships a zstd decompressor only, and there is no static libzstd.a here, so linking it would break the hermetic musl build. Requesting it returns error.CodecUnsupported rather than failing quietly. deflate (0x02, a KERN extension) is implemented and tested.
• Compression and zero-copy are mutually exclusive. Reading a compressed object needs a buffer, so the zero-copy path refuses it explicitly instead of handing back compressed bytes as content.
• QuixBugs 31/31 is execution, not proof — those bugs are caught by running the official test cases, not by a ∀-quantified argument.
• The Refactory numbers are a Python harness, not the KERN core. Two scripts exist; the first reported 83.2 % on buggy files and 83.7 % on correct ones — rates that coincide, so it measured nothing. The second (1705/1782 buggy at 0 false positives on 2442/2442 correct) agrees with the dataset's own test suite, which makes it close to tautological. Neither uses Z3 or the Zig core at all, and the README says so in a footnote.
• 26 of 86 logged defects were "silently broken checks." That is not a brag — it is the base rate I measured while building the harness that catches them.

What it actually costs to adopt

No Zig install, no build step:

curl -fsSL -o kernc https://github.com/newmathphys/kern/releases/download/v2.2.0/kernc-x86_64-linux-musl
chmod +x kernc && ./kernc prove formal/example.smt2

Or as a GitHub Action, one line:

- uses: newmathphys/kern@v2.2.0
  with:
    contract: formal/spec.smt2

Or from an AI agent over MCP (examples/kern_mcp_server.py, stdlib only):

{"mcpServers": {"kern": {"command": "python3",
  "args": ["/path/to/kern/examples/kern_mcp_server.py"]}}}

The MCP server exposes kern_verify_smt, kern_prove_with_checker and
kern_verify_multi_belnap. The last one returns JOIN_K(T, F) = B when two
contracts contradict each other, and refuses to collapse it into a proof.

Why the blunt title

Because the failure mode is not exotic. It is the default outcome of putting an
optimiser (an agent) next to a boolean signal (a green checkmark) with no
independent verifier in between. The agent is not malicious; it is doing exactly
what the signal rewards. The fix is not a better prompt — it is removing the
boolean and replacing it with something that cannot be satisfied vacuously.

1 passed in 0.01s is not a lie. Treating it as proof is.

---

Defect registry: #1–#86. 230 core tests, cross-arch runs on ARM64 and
big-endian POWERPC64, 32 Lean 4 theorems with 0 sorry, 100 % decision coverage.
Every number above is reproduced by make evidence and published under
docs/evidence/.

Comments

[newmathphys]

Quick update — just cut v2.4.0 after running a destructive audit on the new parser, C-ABI, and allocator error paths (pushed our internal defect log from #86 to #103):
github.com/newmathphys/kern/releas...
A few low-level bugs and fixes from this sprint that might be useful to others working with Zig 0.17 and C-ABI:
Testing threadlocal in libkern.so (why zig build test wasn't enough):
In our compat.zig wrapper, if (builtin.is_test) routes I/O straight to std.testing.io at comptime. That meant our threadlocal var tls_io fallback for C/Python callers was completely bypassed during standard Zig unit tests. Writing a standalone C11 stress test (zig cc -Wall -Wextra -Werror -pedantic -std=c11 -pthread) that spawns 8 OS threads hammering libkern.so concurrently (8 × 500 kern_hash + 8 × 20 kern_smt_verify calls) verified the TLS path under actual contention, and -Wpointer-sign immediately caught a char * vs unsigned char * mismatch in include/kern.h (#100) plus missing NULL-pointer guards when len > 0 (#99).
OOM fault injection caught a classic nested-try leak (src/verifier/proof_check.zig):
Running the new S-expression proof checker under a step-by-step failing allocator (fail_index = 0..N) caught a leak in try out.append(allocator, try allocator.dupe(u8, inner)) — when append failed with OutOfMemory, the freshly duplicated slice was orphaned (#101). Also capped recursive S-expr parsing at MAX_SEXP_DEPTH = 4096 after a 2,000,000-paren input blew the stack with SIGSEGV (#98).
Z3 5.1.0 (get-model) quirk & partial unit-resolution:
Added human-readable counterexample extraction ([COUNTEREXAMPLE] amount = -1, balance = 1) when a contract is refuted (SAT). Two Z3 gotchas bit us: calling (get-model) after unsat prints an error that corrupts the stdout stream before (get-proof), and Z3 5.1.0 prints models without an outer (model ...) wrapper (just a bare list of (define-fun ...)). Also fixed our unit-resolution checker to return a 3-state verdict so partial resolution steps emitted by Z3 on (ite ...) branches verify cleanly ([PASS] withdraw_fixed on if/elif/else Python contracts).
CLI --deflate (0x02) & 100% canfail coverage:
Wired std.compress.flate into kernc build --deflate and kernc cat (3.16x compression on our test corpus, verified on read with zip-bomb bounds checking), added kern_verify_python to the stdio MCP server, and expanded the Zig mutation tester from 6 to 14 files (427 mutation sites, 97.5% kill rate, 70/70 Makefile check targets proven capable of failing).