kern MCP server

KERN — a zero-trust verification gateway for AI-generated code

Try it in your browser, offline, right now: docs/playground/ — the real kernc.wasm (wasm32-freestanding, no syscalls) executing JOIN_K, the Fourier–Motzkin solver, the Hamming code and verifyProof on a genuine Z3 certificate — then sabotage one byte of the proof and watch it get rejected. Live: https://newmathphys.github.io/kern/playground/

Three things only KERN catches (verify in 30 seconds)

Each line below is verbatim output of a self-checking demo in this repo. Nothing here is a screenshot: run the command, get the same text, rc=0.

1. Money stolen by rounding — a DeFi fee split. 0.30 % commission on withdrawals; splitting the payment is supposed to cost more, never less.

$ make arbitrage-check
  [FAIL] fee_threshold: no_arbitrage REFUTED — [КОНТРПРИМЕР] a1 = 100, a2 = 1
  [FAIL] fee_floor_capped: no_arbitrage REFUTED — [КОНТРПРИМЕР] a2 = 999, a1 = 1
  [PASS] fee_proportional: no_arbitrage PROVEN (trusted: 0 | holes: 0)
[OK] анти-арбитраж: 2 арбитража поймано, линейная комиссия доказана (trusted: 0)

trusted: 0 means the proof never trusted a helper: no holes, no sorry.

2. Two cloud IAM policies that collide. Data allows reading the bucket; SecOps denies without MFA. A normal engine silently applies "deny wins" and loses one of the two statements. Belnap keeps the contradiction:

$ python3 examples/iam_belnap_conflict.py
  Data   -> T  (Allow READ reports)
  SecOps -> F  (Deny без MFA)
  JOIN_K(T, F) = B
[OK] конфликт сохранён: JOIN_K(T, F) = B -> HTTP 409 Conflict, а не «deny побеждает»

3. An AI agent cheating for a green pipeline. pytest sees nothing; KERN names each trick.

$ python3 examples/rlvr_anticheat_demo.py
  BLOCKED  1. проглоченное исключение      (CHEAT DETECTED)
  BLOCKED  2. выход из теста (exit 0)      (CHEAT DETECTED)
  BLOCKED  3. mock в проверяемом коде      (CHEAT DETECTED)
  BLOCKED  4. подмена константы            (DIVERGED)
  BLOCKED  5. тихий слом края              (DIVERGED)
KERN заблокировал 5/5
[OK] 5/5: награда не куплена — каждый чит назван и заблокирован

Facts (EN/RU, kept in sync by make sync): core 460 · next 53 · catalog 492 · CHECK 212 · cases 258 · anchors 216 · registry 293 · META 58 · Lean 147 · QuixBugs 6/40 SMT + 40/40 diff. Live guide to all 10 capabilities — EN / RU (generated by make demo-all): docs/ALL_CAPABILITIES_LIVE_GUIDE.md · docs/ALL_CAPABILITIES_LIVE_GUIDE.ru.md

Current status snapshot (generated, gated by make status-check): docs/STATUS.md · docs/STATUS.ru.md

KERN applied to KERN (self-verification, verbatim output): docs/SELF_VERIFICATION.md · docs/SELF_VERIFICATION.ru.md

The KERN Charter — every law names its checker, and the checker is run: docs/CHARTER.md · docs/CHARTER.ru.md

Proofs on other people's code — not on our own fixtures: All eight capabilities, one command and one receipt each: docs/PROOF_GALLERY.md · RU Real defects we found, with patches and upstream links: docs/REAL_BUGS_FOUND.md

Blind exam on WHOLE corpora (no file cap, pinned SHAs, 0 edits before the run):

corpus	SHA	files	functions	findings	false	precision
curl/lib	155f6f76	377	430	1	0	1.00
redis/src	5b69ba2c	227	1454	33	0	1.00
tigerbeetle/src	68958eb7	338	120	1	0	1.00
total		942	2004	35	0	1.00

Industrial code where KERN accused NOBODY (0 false alarms): DeepGEMM 144 files · FlashMLA 133 · DeepEP-Ascend 80 · cmark-gfm (known_fp = 0) · actions/toolkit. Honest boundary of the table above: the cap is on the slice, not on the corpus — 2 004 of 10 345 functions were analyzable, the rest were skipped with a NAMED reason (see docs/evidence/blind_p1_2026-11-07.log).

1. EvalPlus MBPP+ — three blind spots of the benchmark itself. Of 264 solutions that passed both MBPP and the 80× MBPP+, --xray flagged three division-by-zero crashes; a live python3 call confirmed all three (Mbpp/265, Mbpp/292, Mbpp/422) and refuted none. 0 false accusations.
2. TheAlgorithms/C (22.5k ★) — a real SIGFPE. math/catalan.c calls factorial(n+1), which returns 0 for n = 0, so the divisor is zero: echo 0 | ./catalan dies with SIGFPE (rc 136) on the unmodified file; from n = 11 it silently prints garbage. Upstream: #1595. Same repository, second report: math/lcm.c printed -35899 where the true lcm(50000, 50000) = 50000 fits in int — #1596.
3. TheAlgorithms/Rust (26k ★) — a u64 underflow. src/math/binomial_coefficient.rs computes n - i with no k <= n guard, so binom(0, 2) panics in debug and returns garbage in release; all seven upstream tests use k <= n. Upstream: #1075 (Codecov: 100% patch coverage).

Every capability, its one command, its external oracle and its honest boundary: docs/CAPABILITY_MATRIX.md · RU Ten proofs, every command verified against this commit: docs/TEN_PROOFS.md · RU — four of the ten examples did not match the repository when first drafted; they are corrected here, and the drifting timing numbers are stated as thresholds, not constants. Resuming work / open items: docs/NEXT_SESSION.md · RU

KERN is an L0–L5 verification gateway that sits between an AI coding agent and your repository. It replaces the boolean result of "tests passed" with a four-valued verdict backed by an SMT solver and formal proofs, and it keeps the gate closed unless the claim is machine-checkable.

Written in Zig 0.17, verified in Lean 4, powered by Z3. Exposes a C-ABI (libkern.so, 8 functions) and an HTTP guardrail proxy.

---

What the agent says — and what KERN proves

make ai-demo drives one realistic agent session end to end. Fixtures live in examples/ai_vs_kern/; every line below is verbatim tool output.

The agent's report	What KERN finds in the same code
2 passed in 0.01s	[CHEAT DETECTED: swallowed assert (except: pass)] line 28 → R=-2.0
"withdrawals cannot increase the balance"	[FAIL] transfer_with_fee: КОНТРАКТ НАРУШЕН · [КОНТРПРИМЕР] result = -1, amount = 1, balance = 0 · [RUNTIME CONFIRMED]
"the commission is fair"	[FAIL] fee_threshold: no_arbitrage REFUTED · [КОНТРПРИМЕР] a1 = 100, a2 = 1
"same behaviour, just cleaner"	[DIVERGED] charge · [КОНТРПРИМЕР] res_old = -1, balance = -1, amount = 0, res_new = 0
"a safe helper tool"	[MCP] PROMPT INJECTION in "sum": «ignore previous» · INVISIBLE UNICODE U+200B
"transfer_funds(900)"	[FAIL] Firewall: POLICY CONFLICT -> B (1,1), e=0, HTTP 409 Conflict

After the fix KERN does not take anyone's word for it — it re-checks the proof in Zig:

[PASS] transfer_with_fee: ДОКАЗАНО
       [PROOF VERIFIED] steps: 50 | premises bound: 3/3 | mp: 17 |
                        rewrite (linear): 18 | farkas: 2 | trusted: 0 | holes: 0
[REWARD] R=+1.0 [VERIFIED REWARD, Belnap T, e=1]

make ai-demo fails (rc=1) if any of those lines disappears, so the demo cannot drift into a claim that the tools no longer back.

---

The problem

AI agents now write code faster than humans can review it. Under pressure to get a green pipeline, they produce two failure modes that no ordinary CI can see:

Failure mode	What CI sees	What actually happened
Vacuous test	✅ 1 passed	The test contains no assert. It cannot fail.
Hallucinated fix	✅ 1 passed	The edge case (amount = -1) was never sampled.

Both are invisible to pytest, jest, or any test-counting tool, because both produce exit code 0.

KERN attacks the gap from two sides:

1. Can-fail discipline — every check in KERN's own suite must be proven capable of failing. A harness (tools/canfail.py) deliberately injects a fault and requires the check to go red. 212 CHECK targets; 212 proven non-vacuous (258 fault-injection cases).
2. Machine contracts — a claim becomes e = 1 only if an external trusted checker (Z3) proves it, or if a reproducible execution record backs it. Text is not evidence.

---

See it in 15 seconds

make run-example      # one hallucinated fix, caught at the Truth Gate
make ai-demo          # the full agent session: cheat, hole, arbitrage, refactor, MCP, firewall

The example (examples/toy_ai_hallucination/) simulates an agent that was asked to fix a withdrawal function. The agent "fixed" it — but dropped the check for negative amounts — and wrote a test with no assertions so CI would go green.

=== [1] Ordinary CI: pytest on the agent's "test" ===
1 passed in 0.01s                      <-- green. The bug ships to production.

=== [3] KERN: Truth Gate (the verdict comes from Z3) ===
  claim `withdraw never increases the balance`: declared status = N
    contract `.../contract_refuted.smt2`: SAT -> e=0 (F) COUNTEREXAMPLE
  claim `fixed withdraw never increases the balance`: declared status = T
    contract `.../contract_fixed.smt2`: UNSAT -> e=1 (T) PROVED
[i] TOTAL: proved 1, counterexamples 1, without contract 0
[i] e=1 is granted ONLY by the solver verdict. Claims without a bound
    contract stay at e=0.

Z3 did not sample inputs. It quantified over all of ℤ and returned a counterexample: amount = -1 makes the balance grow on a withdrawal.

HTTP guardrail proxy

examples/guardrail_proxy.py (stdlib only) exposes libkern.so over HTTP and maps the Belnap B₄ lattice onto distinct RFC 9110 status codes:

Solver / gate verdict	Belnap	HTTP	Meaning
PROVED (UNSAT)	T (1,0)	200 OK	contract holds across the entire domain (e = 1)
REFUTED (SAT)	F (0,1)	422 Unprocessable Entity	counterexample found (e = 0)
UNKNOWN / TOOL_ERR	N (0,0)	422 Unprocessable Entity	timeout or missing solver; fail-closed (e = 0)
CONFLICT (T ⊔ F)	B (1,1)	409 Conflict	contradictory evidence across contracts in /verify_multi (e = 0)

/verify_multi is what exposes the lattice: when one contract returns T and another returns F on the same code, a boolean pipeline either overwrites the status with the last result or conflates an error with a timeout. KERN computes JOIN_K(T, F) = B and answers 409 Conflict.

make guardrail      # self-test on an ephemeral port: 200(T) / 422(F) / 409(B)

---

Verify your own code without writing SMT-LIB

Contracts live in ordinary comments next to the function. No .smt2 files, no solver syntax.

# @kern:requires balance >= 0
# @kern:ensures  result <= balance and result >= 0
def withdraw(balance: int, amount: int) -> int:
    if amount < 0:
        return balance          # if / elif / else are translated to SMT `ite`
    if amount > balance:
        return balance
    return balance - amount

make contracts
# [PASS] withdraw_fixed:      PROVEN  (proof checker: trusted: 0)
# [FAIL] withdraw_missing_neg: CONTRACT VIOLATED
#        [COUNTEREXAMPLE] balance = 0, amount = -1, result = 1
# sum_to_n: SKIP — out of the supported subset (loops)

When a contract is refuted, KERN prints the Z3 counterexample (get-model): the exact input values that break it. Out-of-subset code is reported as SKIP with a reason — never as a silent pass.

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

1. The vacuous precondition (false ⟹ anything). A contradictory requires makes the obligation requires ∧ ¬ensures trivially UNSAT, so any broken body would be reported as proved:

# @kern:requires amount > 10 and amount < 5      # empty domain
# @kern:ensures  result == balance - amount
def withdraw_vacuous(balance: int, amount: int) -> int:
    return balance + amount                      # deliberately wrong

make contracts
# [VACUOUS] withdraw_vacuous: precondition is unsatisfiable (empty domain) -> B4: N, e = 0

2. Weakening the specification instead of fixing the code. The cheapest cheat is to delete the # @kern:ensures line that fails. Every contract is fingerprinted; any removal or edit is a hard error:

make contracts-lock-check
# [SECURITY] sealed contract REMOVED: examples/contracts_demo.py:withdraw:ensures
# rc = 2   (fingerprints are sealed in docs/contracts.lock.json)

3. A refactoring that silently changes behaviour. 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:

make diff-equiv
# [DIVERGED] charge: REFACTORING CHANGED BEHAVIOUR
#            [COUNTEREXAMPLE] amount = 1, res_old = 0, res_new = 2, balance = 1

4. A counterexample that lives only in a log. --emit-pytest turns it into a real regression test that fails on the current code:

python3 tools/kern_contracts.py examples/contracts_demo.py --emit-pytest out_test.py
# def test_counterexample_withdraw_missing_neg():
#     result = withdraw_missing_neg(balance=0, amount=-1)
#     assert (result <= balance)      # FAILS: 1 <= 0 is false

Polyglot contracts, machine types and the GitHub line

5. The extractor is polyglot — the core never was Python-only. kernc prove, the proof checker and libkern.so always took plain SMT-LIB2; only the convenience extractor was Python-only. It now reads the same annotations from .py, .zig, .c and .rs, and because machine types are known it catches what an unbounded Int model cannot:

make contracts
# [PASS] withdrawGuard                      (Zig, i32)
# [FAIL] share: POSSIBLE DIVISION BY ZERO   (C)
#        [COUNTEREXAMPLE] amount = 0
#        [RUNTIME CONFIRMED] division by zero reproduced on those values
# [FAIL] double_it: i32 OVERFLOW            (Rust)
#        [COUNTEREXAMPLE] x = 1073741824, result = 2147483648
#        [RUNTIME CONFIRMED] the computed value 2147483648 is outside [-2147483648, 2147483647]
# [FAIL] withdraw_missing_neg: CONTRACT VIOLATED        (Python)
#        [COUNTEREXAMPLE] balance = 0, amount = -1, result = 1
#        [RUNTIME CONFIRMED] the counterexample really breaks the running function

[RUNTIME CONFIRMED] — all seven languages. For Python the counterexample is replayed by executing the real function. For Zig, C and Rust the extracted body is re-evaluated by an independent concrete evaluator (same statement split, a different computation): if the numbers disagreed with the SMT model, the counterexample would be reported as a translation bug, not as a finding. A compiled replay (zig run / cc / rustc) is not implemented — the evaluator deliberately needs no toolchain, and the tool says nothing it cannot check.

Bit-vector theory (QF_BV) for real systems code. Real functions are full of & | ^ ~ << >>, which do not exist in Int — so addr & ~(alignment - 1), the alignment trick from andrewrk/zig-general-purpose-allocator, used to be skipped. KERN's core has always handled bit-vectors, so the extractor now switches to (_ BitVec 32/64) (bvand, bvnot, bvshl, bvult, ...) — automatically on & | ^ ~ << >>, or explicitly via @kern:bitvec32 / @kern:bitvec64. The same statement parser is reused, so the same code is checked. In this theory overflow is the semantics (the machine wraps), so the overflow obligation is not asserted there; the contract and division-by-zero still are.

Open-source audit gallery (real code, real counterexamples)

Every row below is produced by a run (make audits, tools/bug_hunter.py --trophies), never written by hand. PROVEN means Z3 proved it and our Zig proof checker re-checked the certificate (trusted: 0 | holes: 0); REFUTED comes with the exact Z3 counterexample.

#	Project (file:line)	Claim	Verdict	Counterexample / note
1	ziglang/zig lib/std/mem.zig — alignBackward	addr & ~(alignment-1) == addr - addr % alignment	PROVEN (QF_BV 32)	—
2	same, mutated alignment-2	—	REFUTED	addr = #xffffbffc, alignment = #x00000001
3	ziglang/zig mem.zig — alignForward	addr + (alignment-1) stays in u32	REFUTED	addr = 4294967295, alignment = 2 → 4294967296
4	tigerbeetle/tigerbeetle src/stdx/stdx.zig — div_ceil	(n + d - 1) / d exact & no overflow	PROVEN — 98 steps, trusted: 0	—
5	same, mutated n/d + 1	—	REFUTED	numerator = 2147483647, denominator = 1 → 2147483648 (i32)
6	musl libc src/stdlib/abs.c — abs	result >= 0 for x > INT32_MIN	PROVEN — 51 steps, trusted: 0	—
7	same, guard removed	—	REFUTED	a = -10 → -10
8	ghostty-org/ghostty src/renderer/size.zig — gridColumns	columns never 0	PROVEN	—
9	same, @max(1,…) removed	—	REFUTED	screen_width = 0, cell_width = 1 → 0
10	andrewrk/general-purpose-allocator gpda.zig — isAligned	addr & ~(alignment-1) == addr ⟺ addr % alignment == 0	PROVEN (all 2³² addresses)	—
11	same, alignment-2	—	REFUTED	addr = #xc0000001, alignment = #x40000000
12	zlib zutil.c — zcalloc	items * size fits in u32	REFUTED	items = #x8e0ff0f1, size = #x5ffeffef → #xffffffff
13	JDK (Bloch 2006) binary_search	(low + high) / 2 in i32	REFUTED (QF_BV only)	low = #x804, high = #x7ffff7fc → #xc0000000 (negative)
14	same, low + (high-low)/2	—	PROVEN (Int theory)	—
15	Rust core::num — midpoint	bit-blasted proof	SKIP — honest	the checker does not cover bitBlast
16	Rust saturating_add	clamps to i32 bounds	PROVEN / mutated REFUTED (2147483647 + 1)	—
17	ziglang/zig lib/std/math/ (64 files)	zero-annotation --xray field scan (C-like path)	checked 80 / 219 (was 0)	0 findings after fixing #159/#160
18	Python 3.12 stdlib (urllib, http, email, datetime, ipaddress, decimal, fractions, statistics)	--xray field scan	checked 211 / 413, 0 false positives	0 findings on production code after fixing defects #134/#158

Honest limits of this table. (a) The SMT model is ours: a counterexample must still be reproduced against the project's own build before it can be called their bug. (b) Bloch's bug is invisible in the Int theory — it needs @kern:bitvec32 (QF_BV). (c) SKIP rows are kept on purpose: a verifier that never refuses is not verifying.

What KERN is — and what it is not. KERN is a verification gate for contracts: it proves requires ⇒ ensures, re-checks the solver certificate with its own Zig checker (trusted: 0), and refuses to open the gate without that certificate. It is not a replacement for an AST-level linter on unannotated C/C++: zero-annotation --xray for C-like languages parses conditions, guards and divisors (plus two C-specific classes — a possibly negative index [BOUNDS PATH] and a size that can overflow INT32_MAX before an allocation [OVERFLOW PATH]), and on real repositories it reaches 173/182 (95.1 %) of functions with branches in cmark-gfm and 72/77 (93.5 %) in actions/toolkit, at 0 false accusations (measured at v2.8.1; the earlier front end, before that release, skipped 60–80 % of functions — 95/254 and 32/148). A 0 findings row therefore means "nothing proven and nothing refuted inside the analysed subset" — not "the code is clean". A retro-test on four published cmark-gfm security fixes caught 1 of 4 (the OOB read in validate_protocol) with 0 false accusations on the fixed file — see docs/FIELD_AUDIT_REPORT.md §4.

--full-scan <path> runs the honest subset in one pass: --xray over 7 languages (dead branches, crash paths, negative index, size overflow), --anti-cheat over all .py, and --audit-mcp when a manifest exists. Theories that need a contract (QF_S, IEEE-754, no_arbitrage, 2-Safety, --loops) are printed as applicable — needs contract (@kern:…), not evaluated; they are never mixed with findings.

Two modes, never conflated. With a law (@kern:requires / @kern:ensures, or a project KERN.md) KERN is deciding: it prints PROVEN or CONTRACT VIOLATED plus a counterexample that a live run confirms. Without a law, --xray is a hint about a hidden precondition: it knows only the declared type, so for int it substitutes the type extremes (e.g. INT_MIN), and the warning means "this function needs a precondition to be safe" — not "this repository has a bug". The cleanest demonstration: the correct midpoint low + (high - low) / 2 still gets an [OVERFLOW PATH] in --xray, because without the law high >= low the tool must consider high = INT_MIN, low = INT_MAX. An upstream report therefore requires a violation that reproduces through a public call on a normal input, never a raw --xray line. Walkthrough with live output: docs/АНАТОМИЯ_ДОКАЗАТЕЛЬСТВА.md.