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

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.

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:

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. 65 checks; 64 proven non-vacuous.
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

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:

/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:      ДОКАЗАНО  (proof checker: trusted: 0)
# [FAIL] withdraw_missing_neg: КОНТРАКТ НАРУШЕН
#        [КОНТРПРИМЕР] 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: предусловие ПРОТИВОРЕЧИВО (пустой домен) -> 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] контракт УДАЛЁН: 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: РЕФАКТОРИНГ ИЗМЕНИЛ ПОВЕДЕНИЕ!
#            [КОНТРПРИМЕР] 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: ВОЗМОЖНО ДЕЛЕНИЕ НА НОЛЬ   [КОНТРПРИМЕР] amount = 0
# [FAIL] double_it: ПЕРЕПОЛНЕНИЕ типа i32  [КОНТРПРИМЕР] x = 1073741824, result = 2147483648
# [RUNTIME CONFIRMED] the counterexample really breaks the running function

6. KERN verifies itself: make self-verify puts contracts on the formulas
the kernel actually uses (payloadSlice offsets, the Farkas negation identity
¬(l ≤ r) ↔ r - l + 1 ≤ 0 from proof_check.zig) and proves them with Z3.

7. The GitHub line and a Git gate:

make sarif-check   # SARIF 2.1.0 -> Code Scanning / red squiggle under the buggy line
make hook-check    # self-test of the pre-commit gate
python3 tools/kern_contracts.py --install-hook   # blocks `git commit` on a broken contract

The released attestation is signed with Ed25519 (kern.intoto.sig, the
owner key already used by src/attest.zig), so slsa_provenance.py --check
detects a substituted attestation — the old “unsigned (no cosign)” gap is closed.

For AI agents, examples/kern_mcp_server.py exposes the gate over the Model
Context Protocol (5 tools: kern_verify_smt, kern_prove_with_checker,
kern_verify_multi_belnap, kern_verify_python, kern_check_equivalence —
the last one proves a refactoring preserves behaviour without writing any
contracts):

{"mcpServers": {"kern": {"command": "python3",
  "args": ["/path/to/kern/examples/kern_mcp_server.py"]}}}

make mcp-selftest   # drives the server over stdio: 12 live checks, all 5 tools

Core ideas

Belnap B₄ logic — results accumulate, they never overwrite

Each claim carries two independent support channels: p (positive) and n
(negative).

A newly passing test joins with history, it does not replace it:

JOIN_K(T, F) = B        -- a conflict can never be silently resolved into a pass

This is the mechanism that makes "one green run" unable to hide a previously
observed failure. (Defect #46 in the project's own registry was exactly the
opposite behaviour — status overwrite — and was found by the can-fail harness.)

The Gate is closed by default

e = 1  <=>  policy allows  AND  provenance hash matches  AND  checker verdict = SUCCESS
            AND  Belnap status = T  AND  coverage complete  AND  no scope ambiguity

Timeout, missing solver, unknown answer, or a fake textual witness all yield
e = 0. The AI's own witness_payload never influences the verdict — only
the external trusted checker does.

Architecture (L0 – L5)

flowchart LR
    Agent["AI agent / PR<br/>(code + @kern:spec)"]

    subgraph KERN ["KERN verification gateway (Zig 0.17, libkern.so)"]
        direction LR
        L0["L0-L2: .kimg + KERNFS<br/>Merkle, BLAKE3 default"]
        L4["L4: Z3 SMT bridge<br/>QF_LIA/BV/AX/S/FP, CHC"]

        T["T (1,0)<br/>proved"]
        F["F (0,1)<br/>refuted"]
        N["N (0,0)<br/>no evidence"]

        B4["L3: Belnap B4<br/>JOIN_K(T,F) = B"]
        Gate{"Truth gate<br/>policy + provenance"}

        L0 --> L4
        L4 -->|"UNSAT"| T
        L4 -->|"SAT (counterexample)"| F
        L4 -->|"timeout / no contract"| N

        T --> B4
        F --> B4
        N --> B4
        B4 --> Gate
    end

    HTTP200["e = 1 : HTTP 200 OK<br/>belnap = T (admitted)"]
    HTTP422["e = 0 : HTTP 422 Unprocessable<br/>belnap = F | N (refuted / fail-closed)"]
    HTTP409["e = 0 : HTTP 409 Conflict<br/>belnap = B (T and F coexist)"]

    Agent --> L0
    Gate -->|"status == T"| HTTP200
    Gate -->|"status in {F, N}"| HTTP422
    Gate -->|"status == B"| HTTP409

    HTTP422 -.->|"Z3 counterexample"| Agent
    HTTP409 -.->|"conflict diagnostic"| Agent

    classDef darkBox fill:#0d1117,stroke:#30363d,stroke-width:1.5px,color:#c9d1d9
    classDef gateBox fill:#161b22,stroke:#58a6ff,stroke-width:1.5px,color:#f0f6fc
    classDef passBox fill:#0f2d1e,stroke:#238636,stroke-width:1.5px,color:#3fb950
    classDef warnBox fill:#2d210f,stroke:#d29922,stroke-width:1.5px,color:#e3b341
    classDef failBox fill:#3d1318,stroke:#f85149,stroke-width:1.5px,color:#ff7b72

    class Agent,L0,L4,N,B4 darkBox
    class Gate gateBox
    class T,HTTP200 passBox
    class F,HTTP422 warnBox
    class HTTP409 failBox

The verification engine (kernx, "KERN-Next") reads a .kern project DSL and
produces a SQLite catalogue, snapshots, diffs, reports and an agent hand-off
packet.

Embedding

/* include/kern.h — 8 exported functions */
int kern_smt_verify(const unsigned char *smt, unsigned long len);
int kern_kimg_valid(const unsigned char *img, unsigned long len);
long kern_kimg_object_count(const unsigned char *img, unsigned long len);
int kern_localize(const unsigned char *decls, unsigned long decls_len, ...);
int kern_hash(unsigned int algo, const unsigned char *data, unsigned long len,
              unsigned char *out32);

kern_hash is the single source of truth for digests: the Python tooling calls it
through ctypes, so client and kernel cannot diverge (verified: kernel BLAKE3 and
the reference implementation produce identical digests).

The HTTP guardrail (examples/guardrail_proxy.py, stdlib only) maps the Belnap
lattice onto HTTP status codes:

Measured, not claimed

Everything below was produced by a real run on Zig 0.17.0. Reproduce with
make test-all, make audit-manifest, make canfail.

Core health

Cross-architecture

External benchmarks

On the Refactory row (defect #77, found 2026-10-16). Two Python-only
harnesses exist for this dataset, and neither uses the KERN core
(kernc, Z3, Lean) - they are differential execution scripts:

1. tools/refactory_diff.py compares a candidate against reference.py on
   random inputs. Measured on the full dataset: 1482/1782 (83.2%) of buggy
   files diverge, but so do 2045/2442 (83.7%) of the files the dataset labels
   correct. The two rates coincide, so this number does not measure
   detection quality - it was previously reported in this README without the
   false-positive side.
2. tools/refactory_suite.py uses the dataset's own test suite
   (ans/input_NNN.txt + output_NNN.txt), which is what the labels are
   defined by. Against that oracle, one and the same run gives:
   buggy 1705/1782 (95.7%) with 0 false positives on the correct set
   (2442/2442). This is close to tautological, since the labels are the
   suite. (An earlier intermediate run reported 1736/1782, but that was
   measured before two harness bugs were fixed - shared mutable arguments and
   repr()-based comparison instead of the dataset's == semantics - and on
   that run the correct side was broken, 290/2442. See docs/METRICS.md 50.3.)

Conclusion: the Refactory numbers describe an external Python harness, not
the formal verifier, and are therefore not listed as a core metric.

| CHC / Horn (loop invariants) | 11 / 11 | no |
| SMT-LIB (official suite) | 1104 / 1104 verdicts matched, 0 divergences, 0 false accepts | no |
| HumanEval / HumanEval+ (EvalPlus) | 0.524 / 0.500 | yes (API) |
| MBPP / MBPP+ (EvalPlus) | 0.812 / 0.698 | yes (API) |

Scope of the static gate. In the HumanEval experiment the static gate blocked
55 samples; all 55 genuinely failed (100 % precision), but it did not raise
pass@1. A static gate fires before execution and cannot repair logic. Raising
the score requires execution evidence, not AST inspection.

Performance

Hash primitive in isolation (make bench-hash, docs/evidence/hash_bench.log):

The ~230× gap between raw addressing and verified read is the cost of hashing every
byte — and it is the reason a tampered payload cannot be served. SHA-NI is not
available on the reference CPU (Intel i7-7700, Kaby Lake), so the primitive speed
comes from BLAKE3's AVX2 path.

Reproducibility (measured)

Two clean builds each (rm -rf .zig-cache in between):

Quick start

Requirements: Zig 0.17.0, Python 3.12+, z3 (via pip install z3-solver),
and Lean 4 (only for formal/).

# 1. Toolchain (Zig 0.17.0)
export PATH="$HOME/opt/zig-x86_64-linux-0.17.0:$PATH"

# 2. Build: kernc (core CLI), kernx (KERN-Next), kern-attack (attack demo)
zig build

# 3. Core test suites
zig build test          # 279 core tests
zig build test-next     # 37 KERN-Next tests

# 4. The 15-second demo: green CI vs. mathematics
make run-example

# 5. HTTP guardrail: Belnap lattice on status codes (200 / 422 / 409)
make guardrail

# 6. Prove a contract with real Z3
uv pip install --python .venv/bin/python z3-solver
./zig-out/bin/kernc prove formal/example.smt2

# 7. Formal proofs (Lean 4): 8 files, 42 theorems, 0 sorry
./formal/setup_mathlib.sh    # one-time: fetch prebuilt Mathlib
./formal/check.sh

# 8. Full qualification manifest — every line is a real run
make audit-manifest

One command for everything:

make test-all      # build + tests + UB detector + SMT + perf + mutation
make canfail       # prove that every check is capable of failing
make evidence      # re-run every check and store its log in docs/evidence/

Docker

docker build -t kern:2.0 .
docker run --rm kern:2.0                        # integrity check on the golden image
docker run --rm kern:2.0 verify /kern/toy.kimg  # run the Truth Gate

Prebuilt static binary and GitHub Action

No toolchain needed. Release v2.4.0 ships a statically linked x86_64-linux-musl
binary (6,041,776 bytes), so kernc runs on any x86-64 Linux without Zig:

curl -fsSL -o kernc \
  https://github.com/newmathphys/kern/releases/download/v2.4.0/kernc-x86_64-linux-musl
chmod +x kernc && ./kernc --version
# verify the download first:
# 75b1a8a00404a23e95889e49503d741e65f0ed84235077f4f370b3501ea0b9a5  kernc-x86_64-linux-musl

Or use it as a step in your own workflow:

- uses: newmathphys/[email protected]
  with:
    args: verify --image project.kimg

The Action is a thin wrapper: it downloads the same static binary and runs it.
The .kimg image itself is still produced by the build steps above.

Certification package

For safety-critical and regulated environments (formal/certification/):

Mapped to DO-178C / DO-333 (DAL A), ISO 26262 (ASIL D), Common Criteria
EAL6+/EAL7, FIPS 140-3 and ACID / crash consistency — with the evidence
file backing each row.

Known limitations

A claim without evidence is not a claim. Applying that rule to this project:

• Z3 is an external dependency. If it is absent, the Gate stays closed
  (e = 0) — safe degradation, not a failure.
• Debug builds are not bit-reproducible under Zig 0.17 (non-deterministic
  DWARF). Attested artefacts are ReleaseFast. See the table above.
• The static gate does not raise pass@1. It has 100 % precision and ~70 %
  recall on the HumanEval set; it removes bad code, it does not improve good code.
• The solver proof is re-checked, but Alethe is not available.
  src/verifier/proof_check.zig parses the proof Z3 actually emits and re-checks
  it: hole rejection, premise binding against the contract, mp structure,
  unit-resolution literal coverage, and Farkas arithmetic certificates. Two
  honest limits remain: (a) Alethe/LFSC is not produced by this Z3 build
  (strings z3 | grep -ic alethe -> 0, no proof.format option), so only the
  native format is checked; (b) rewrite steps are re-verified only where the
  normalizer covers them - elementary comparison identities (reflexivity,
  (<= a b) == (>= b a), (> a b) == (not (>= b a)), (< a b) == (not (>= a b))).
  On the reference proof this closes all 5 rewrite steps (rewrite_verified = 5,
  trusted_steps = 0); a rewrite whose two sides both normalize but are not
  equal is reported as rewrite_bad and rejected. Beyond comparisons and
  linear arithmetic, refl/symm/trans, and-elim, not-or-elim,
  monotonicity and Boolean normalization (De Morgan, equality expansion) are
  verified too, so kernc prove formal/example.smt2 prints trusted: 0 - all
  16 steps of that DAG are re-checked independently. Identities that need term
  arithmetic (like-term collection, distributivity) stay in trusted_steps and
  are never reported as verified.
• No hardware attestation. The Ed25519 ownership/attestation pipeline is
  implemented in software; there is no TPM/SGX integration (no such hardware here).
• SLSA attestation is unsigned (no cosign in the environment) — structurally
  valid, but not SLSA Level 3.
• Object compression. deflate (codec 0x02) is implemented via Zig's own
  std.compress.flate and covered by end-to-end tests; compression_codec,
  compressed_size and uncompressed_size are now real fields, not placeholders.
  zstd (codec 0x01) remains declared but NOT implemented — Zig std ships a
  zstd decompressor only, and no static libzstd.a exists here, so linking it
  would break the hermetic musl build. Requesting it returns
  error.CodecUnsupported rather than failing silently.
  Note that compression and zero-copy are mutually exclusive by nature: reading a
  compressed object requires a buffer, so payloadSlice refuses it explicitly
  (CompressedNeedsDecompress) and callers use decompressObject.
• One can-fail meta-control case can report rc=2 under Zig cache contention;
  the harness retries once and reports it separately from real vacuous checks.
• The full list lives in formal/certification/KNOWN_LIMITATIONS.md and
  docs/CAPABILITY_STATUS.md.

Repository layout

src/            Zig core: .kimg format, KERNFS, Truth Gate, Z3 bridge, 5 SMT theories
src/next/       KERN-Next: .kern DSL, SQLite catalogue, snapshots, agent hand-off
formal/         Lean 4 proofs (42 theorems) + certification package
examples/       toy_ai_hallucination/ demo, guardrail_proxy.py HTTP guardrail
tools/          can-fail harness, mutation tester, benchmarks, cross-arch runner
docs/           specification, METRICS.md, TEST_CATALOG.md, capability status, evidence/

Key documents

Contributing

Read CONTRIBUTING.md. The golden rule: if your check cannot
fail, it is not a check. Every new test must survive the can-fail harness.

Security issues: see SECURITY.md.

License

Copyright (c) 2026 Vital Kalinousky. All rights reserved.

KERN is source-available, dual-licensed:

1. PolyForm Noncommercial License 1.0.0 (PolyForm-Noncommercial-1.0.0) —
   free of charge for any noncommercial purpose: personal use, hobby
   projects, study, research, teaching, and use by charitable organizations,
   educational institutions and public research bodies. Full text in
   LICENSE.
2. Commercial license from the copyright holder (Vital Kalinousky, [email protected]) —
   required for any commercial use. This explicitly includes running
   kernc, kernx or libkern.so in a company's internal CI/CD pipeline,
   even when nothing is exposed to the public, as well as embedding the
   verification gateway into a commercial product or a paid service.

Note: this is not an open-source license as defined by the OSI. Commercial
use without a commercial license is not permitted.

SPDX-License-Identifier: PolyForm-Noncommercial-1.0.0 OR LicenseRef-KERN-Commercial

Contributions are accepted under the terms in CONTRIBUTING.md
(dual-licensing grant).