KERN Adds a Zero-Trust Verification Gate for AI-Generated Code

Summary

KERN is a source-available verification gateway designed to sit between an AI coding agent and a repository. It replaces a simple “tests passed” result with a four-valued Belnap B4 verdict backed by external machine evidence, keeping admission closed unless policy, provenance, coverage, and checker conditions are satisfied. Its Zig 0.17 implementation exposes a C ABI and an HTTP guardrail proxy, while Z3 handles SMT contracts and Lean 4 contains 32 theorems across seven files with no `sorry`. The project’s example contrasts ordinary CI with formal checking: a withdrawal test with no assertions passes in pytest, but Z3 finds that a negative amount can increase the balance, producing a counterexample; the corrected contract is admitted only after an UNSAT result. KERN combines positive and negative evidence rather than overwriting earlier results, so contradictory contracts become `B` and map to HTTP 409, while proved, refuted, and unknown results map to distinct fail-closed responses. Reported runs include 204/204 core tests in Debug and ReleaseSafe, 37/37 KERN-Next tests, no reported memory or file-descriptor leaks, 100% decision coverage, and a 92.5% mutation score. On external checks, it reports 31/31 QuixBugs cases found, 1104/1104 SMT-LIB verdicts matched, and static blocking of 55 HumanEval samples with 100% precision; the static gate did not improve pass@1. The project documents important limits: Z3 is an external dependency, Debug builds are not bit-reproducible because of Zig DWARF, Alethe proofs are unavailable, hardware attestation is absent, and the SLSA attestation is unsigned. Commercial use requires a separate license, while noncommercial use is covered by PolyForm Noncommercial 1.0.0.