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-muslin 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 -3withoutpipefail— the pipeline reported the status oftail, so a failing proof check looked green; -
kernc cat image /raw/missingprinted data to stderr and exited0, sokernc cat ... > out.txtproduced an empty file and no error; - a
.gitignorerule*.logplaced after!docs/evidence/*.logsilently 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 ≤ 0normalisation over ℤ (where most hand-written checkers silently get the sign or the+1wrong); - 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. -
zstdis declared in the format and NOT implemented. Zig's std ships a zstd decompressor only, and there is no staticlibzstd.ahere, so linking it would break the hermetic musl build. Requesting it returnserror.CodecUnsupportedrather 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/[email protected]
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/.
Top comments (4)
KERN v2.7.3 — Zero-Trust Formal Verification Gateway (Zig 0.17 + Z3 + Lean 4)
• 147 Lean 4 theorems (0 sorry) · 436 core tests (x86_64, ARM64, PPC64 BE)
• 164/164 CHECK gates · 196 non-vacuous can-fail cases · 1,225/1,225 mutants killed
• NIST Juliet / SV-COMP paired benchmark: Youden J = 1.00, score 27/27 (0 penalty)
• QuixBugs symbolic diff: 40/40 DIVERGED, 0 false equivalents · AI-Traps: 6/6 caught
• Upstream bugs found & PRs submitted: TheAlgorithms/C (#1595, #1596), TheAlgorithms/Rust (#1075)
• Independently verified on release binaries (PHI-OMEGA / M: 0/1,680 translation mismatches)
Here is the comprehensive, industrial-grade architectural diff and changelog comparing KERN v2.4.0 (frozen on GitHub at commit
28e6bb9) and KERN v2.5.0 (accumulated across 134+ commits onv2.5-devup toHEAD: 1bab8c2):🛡️ KERN v2.4.0 vs v2.5.0: Complete Architectural Diff & Comparative Analysis
📊 1. Metric-by-Metric Comparison
v2.5-devHEAD)28e6bb9)kernxEngine Testssorry)kernc.wasm)🔬 2. The Seven Core Qualitative Breakthroughs in v2.5.0
1. Autonomous Native LIA Solver in Pure Zig (
builtin_lia.zig)e = 0).2. Complete Elimination of Trusted Proof Steps (
trusted: 0 | holes: 0)musl abs.cbenchmark remained asSKIP(trusted: 15). IEEE-754 floating-point proofs relied ontrusted: 213, and string theory relied ontrusted: 9.musl abs.c$\to$trusted: 0 | holes: 0(all 51 DAG steps verified).trusted: 0 | holes: 0(reduced from 213 to 0).trusted: 0 | holes: 0(reduced from 9 to 0).intro-defwith occurs-check), RAA hypothesis discharge (lemma), propositional tautology elimination (def-axiom), and discrete integer disjunctive splitting ($X \ne Y \iff X < Y \lor X > Y$).3. Zero-Annotation Code Doctor (
--xray&--gen-tests)# @kern:requires/@kern:ensuresannotations. On unannotated or legacy code, KERN reported "0 functions checked".--xraymode: Evaluates raw, unannotated code. Tracks AST path conditions (including path-narrowing after sequentialif ...: return), mathematically proving[DEAD BRANCH](UNSAT reachability),[REDUNDANT GUARD], and[CRASH PATH](division by zero, integer overflows).--gen-testsmode: Queries Z3 models for every reachable path, synthesizing standalonepytestsuites providing 100% branch coverage out of the box.4. Universal Repository Auditor (
kernc audit-repo)kernc audit-repo <local_path | github_url>:/dev/shm) with strict sandboxing (Git hooks disabled viacore.hooksPath=/dev/null, LFS blobs ignored, symlink loops prevented).SIGTERM/SIGINT(Defect #156).--html-out).5. In-Browser WASM Playground (
docs/index.html+docs/kernc.wasm)wasm32-freestanding). Visitors tohttps://newmathphys.github.io/kern/can paste raw code or any GitHub URL: the browser executes Fourier-Motzkin LIA and Belnap $B_4$ lattice operations directly on the client side in <0.2 ms without server roundtrips.6. AI Threat Shield & Anti-Reward Hacking
__eq__ -> True,sys.exit(0), and productionmockpatches used by AI to fake green CI runs.U+200B), and seals configurations viamcp-tools.lock.jsonagainst dynamic rug-pull attacks.409 Conflict,422 Unprocessable) validating agent tool calls against financial policies before network execution.7. Exhaustive 100.0% Mutation Testing Milestone (1,225 / 1,225)
sha256(seed : file : text : mutation)./dev/shmcapacity exhaustion via_trim_slot_cache(), eliminating false-positive compiler kills.🛠️ 3. Critical Kernel Defects Caught by the Self-Testing Harness
The self-testing harness (
canfail, mutator, OOM injection) caught and fixed 35 real defects (#123–#162) during this cycle, including:sealImageRootandcomputeImageMerkleRoot.pcc-checkwhereproof_concludes_falsemasked verification failures.--gen-teststook the buggy function as its ground truth.ffi-bridge-checkwhere the mutator patched the wrong verification path.--xrayso sequentialif ...: returnstatements properly invalidate unreachable subsequent conditions.SIGTERM/SIGINTtraps and atomicos.replacerollbacks to prevent dirty git trees when tests time out.[CRASH PATH]warnings on IEEE-754 floating-point divisions by zero (which yield±inf, not panics).🏁 Summary
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).
Another major update to v2.4.0 (61b341c) — we expanded the formal proofs, made the contract extractor polyglot, and closed four classic "specification gaming" traps that AI agents use to bypass verification:
github.com/newmathphys/kern