KERN

ZIG 0.17 / Z3 / LEAN 4

L0-L5 verification gateway / sealed .kimg container

Belnap B4 truth gate / polyglot @kern: contracts / MCP server

A claim is admitted only with machine evidence.

Download static binary (v2.4.0) Read the README Documentation

KERN architecture: Belnap B4 accumulator, L0-L5 engine and truth gate, measured baseline

What K.E.R.N. stands for

K.E.R.N. — KNOWLEDGE EVALUATION AND RESOLUTION NODE

KKnowledge — everything an AI agent produces: code, contracts, tests, AST trees. KERN treats it as a claim, not as a fact. EEvaluation — mathematical checking of that claim: Z3 SMT, an independent proof-DAG checker written in Zig, and theorems in Lean 4. RResolution — resolving the conflict between old and new knowledge in Belnap's four-valued logic, where a contradiction is kept as T ⊔ F = B instead of being silently overwritten. NNode — the single gateway (an L0–L5 firewall): code either reaches production with e = 1 or is blocked with e = 0.

See it in 15 seconds

bash — make run-example (real transcript)

█

Transcript of a real make run-example run. Command lines, verdict tokens (SAT/UNSAT, e=0/e=1, (F)/(T)) and numbers are printed verbatim; the surrounding prose is shown in English for readability — the tool itself prints Russian verdict words, and the can-fail gates depend on those exact strings.

What it is

A gate, not a linter. Text is not evidence: a claim becomes e = 1 only if Z3 proves it, or if a reproducible execution record backs it.
Bidirectional distrust of the solver. Every UNSAT proof DAG is re-checked inside Zig (proof_check.zig); every SAT counterexample is re-checked too — for Python by executing the real function, for Zig/C/Rust by an independent concrete evaluator over the extracted body (a mismatch would be reported as a translation bug, not as a finding).
Polyglot contracts. @kern:requires / @kern:ensures are read from .py, .zig, .c and .rs — with machine types, so i32 overflow and division by zero are caught.

Try it in one line — no Zig required

DOCKER · VERIFIED 2026-10-17 · IMAGE 364 MB

docker build -t kern:2.4.0 .                       # context ~4.3 MB (.dockerignore)
docker run --rm kern:2.4.0                         # integrity check: header + Merkle root
docker run --rm kern:2.4.0 verify /kern/toy.kimg   # the Truth Gate

# the last command really prints (verdict tokens verbatim):
#   claim `withdraw never increases the balance`
#     SAT -> e=0 (F)    COUNTEREXAMPLE — the agent's claim is refuted
#   claim `fixed withdraw never increases the balance`
#     UNSAT -> e=1 (T)  PROVEN by Z3, re-checked by the proof checker

Built and executed with Docker Engine 29.8.1 (overlayfs) — the two outputs above come from that run. The build is multi-stage: Zig 0.17.0 compiles kernc; the runtime stage ships it together with z3 and a pre-built toy image.

Or the static binary — and verify what you downloaded

# 1. Download the static binary (musl) and VERIFY its checksum before running it
curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.4.0/kernc-x86_64-linux-musl
curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.4.0/SHA256SUMS
sha256sum -c SHA256SUMS          # supply-chain check, no trust required
chmod +x kernc-x86_64-linux-musl

# 2. Prove a contract with real Z3
./kernc-x86_64-linux-musl prove formal/example.smt2   # e=1 PROVEN / e=0 counterexample

# 3. From source
git clone https://github.com/newmathphys/kern && cd kern
zig build && zig build test   # 279 core tests
make contracts                 # polyglot @kern: contracts (Python / Zig / C / Rust)
./formal/check.sh              # Lean 4: 8 files, 42 theorems, 0 sorry

Measured, not claimed

MEASURED BASELINE

279 / 279core tests (Debug + ReleaseSafe) 38 / 38KERN-Next tests 95.0 %mutation score — 38/40 killed, 2 proven equivalent (14 files / 420 sites) 79 / 79can-fail CHECK targets — 94 non-vacuous cases, 0 vacuous

42 / 0Lean 4 theorems / 0 sorry (8 files) 100.0 %decision coverage (30/30) 240/4/0QEMU ARM64 + POWERPC64 passed / skipped / failed (re-run pending) 6 041 776 Bhermetic release binary, sha256 verified (README == build == asset)

Every number above is produced by a command you can run yourself — see docs/METRICS.en.md and docs/evidence/. Exact per-commit metrics (avalanche, collision chain, χ²) are charted on the benchmark page.

Four traps an AI agent falls into — and how KERN refuses them

Vacuous precondition (false ⟹ anything): a contradictory requires would make any broken body "provable" → KERN answers [VACUOUS] precondition is unsatisfiable (empty domain) and keeps the gate closed.
Weakening the specification: deleting a failing @kern:ensures is the cheapest cheat → every contract is fingerprinted in docs/contracts.lock.json, and any removal or edit is a hard error (rc = 2).
Silent behaviour change during refactoring: no contracts required → KERN checks ∃x: f_old(x) ≠ f_new(x) over all of ℤ and prints the exact input where the two versions disagree.
A counterexample that lives only in a log: --emit-pytest turns it into a real regression test that fails on the current code, while --sarif / --github-annotations put it on the exact line inside a pull request.

For AI agents (MCP) and CI

Five tools over stdio for Claude Code / Cursor and any MCP client, with 14 live self-checks (make mcp-selftest): kern_verify_smt · kern_verify_python · kern_check_contracts · kern_prove_contract · kern_check_equivalence.

In CI, the reusable Action verifies the downloaded binary against SHA256SUMS before running it, and can emit a SARIF 2.1.0 report for GitHub Code Scanning:
uses: newmathphys/kern@v2.4.0

Defect Journal — when the checks themselves lied

Short entries from docs/METRICS.md; the full registry is 75 entries, #1–#117. Each entry is a case where a measurement or a harness was wrong — not the code it was checking.

#110 — the mutation score was measured without a solver.

Symptom: the score "dropped" to 77.5 % after the mutator was pointed at 14 files instead of 6. Found by measuring, not guessing: without z3 in PATH the suite reports 263 passed; 8 skipped — and a skipped test cannot kill a mutant. One of those 8 tests had been written specifically to kill the mutant that "survived". Fix: the mutator now requires a solver (--require-solver); the honest score is 95.0 % (38/40).

#107 — 64 % of the mutants came from a single file.

Symptom: "mutation coverage over 14 files" — but proof_check.zig holds 266 of the 420 sites, so a uniform sample put ~25 mutants in one file and 0–1 in the others. Fix: stratified sampling with a guaranteed minimum per file, a fixed recorded seed, and the site distribution published in the defect entry.

#116 — the harness rollback silently discarded an edit made during a run.

Symptom: a README edit vanished, and the file stayed syntactically valid, so nothing looked broken. Found by comparing content, not exit codes: the can-fail harness restores patched files from a byte snapshot taken at the start of each case — and for files the case itself patched, a third-party edit in between was overwritten without a word. Fix: the harness records the hash of what it wrote and refuses to restore when the file changed afterwards; per-case state is reset. Verified by a targeted 3/3 test.

Honest status

What is measured, what is written but not measured, what is not implemented and what is not verified for real is listed in CAPABILITY_STATUS.en.md, together with the 75 defects this project found in itself (#1–#117). A check that cannot go red is treated as a defect here, not as coverage.