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

Факты (EN/RU, синхронизируются make sync): core <!-- fact:core_tests -->441 · next <!-- fact:next_tests -->53 · catalog <!-- fact:catalog -->470 · CHECK <!-- fact:check_targets -->160 · cases <!-- fact:canfail_cases -->190 · anchors <!-- fact:anchors -->150 · registry <!-- fact:registry_targets -->211 · META <!-- fact:meta_targets -->37 · Lean <!-- fact:lean_theorems -->147 · QuixBugs <!-- fact:quixbugs.smt -->6/40 SMT + <!-- fact:quixbugs.differential -->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

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. 160 CHECK targets; 160 proven non-vacuous (190 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 coun