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)

newmathphys — Fri, 16 Oct 2026 11:55:55 +0000

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/.

DEV Community: newmathphys