newmathphys/kern

> Факты (EN/RU, синхронизируются make sync): core 460 · next 53 · catalog 491 · CHECK 185 · cases 225 · anchors 183 · registry 241 · META 41 · Lean 147 · QuixBugs 6/40 SMT + 40/40 diff.
> Live guide to all 10 capabilities — EN / RU (generated by make demo-all): docs/ALLCAPABILITIESLIVEGUIDE.md · docs/ALLCAPABILITIESLIVEGUIDE.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/SELFVERIFICATION.md · docs/SELFVERIFICATION.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:
> 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/binomialcoefficient.rs computes n - i with no k
> Every capability, its one command, its external oracle and its honest boundary: docs/CAPABILITYMATRIX.md · RU
> Ten proofs, every command verified against this commit: docs/TENPROOFS.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/NEXTSESSION.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/aivskern/; 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] transferwithfee: КОНТРАКТ НАРУШЕН · [КОНТРПРИМЕР] result = -1, amount = 1, balance = 0 · [RUNTIME CONFIRMED] |
| "the commission is fair" | [FAIL] feethreshold: noarbitrage REFUTED · [КОНТРПРИМЕР] a1 = 100, a2 = 1 |
| "same behaviour, just cleaner" | [DIVERGED] charge · [КОНТРПРИМЕР] resold = -1, balance = -1, amount = 0, resnew = 0 |
| "a safe helper tool" | [MCP] PROMPT INJECTION in "sum": «ignore previous» · INVISIBLE UNICODE U+200B |