KERN is a verification gateway: it decides whether a claim about code is admissible (e = 1) or not (e = 0). A defect in KERN is security-relevant when it can make the gate accept something it should reject — a false accept.

The following are the highest-severity classes for this project:

Security fixes are applied to the active line only.

Please do not open a public issue for security-relevant findings.

Report privately through GitHub's private vulnerability reporting on this repository (Security → Report a vulnerability).

If that channel is unavailable, contact the maintainer listed in README.md / LICENSE.

1. The exact command and input that triggers the issue.
2. The observed behaviour and the expected behaviour.
3. Which invariant is violated (e = 1 without proof, tampered payload served, crash, hang, leak).
4. Whether the issue is reachable from untrusted input (a .kern project, a .kimg image, an .smt2 contract).
5. If possible, a minimal reproducing artifact.

Credit will be given in the defect registry (docs/CAPABILITY_STATUS.md) unless you prefer to stay anonymous.

These are documented, deliberate boundaries (see formal/certification/KNOWN_LIMITATIONS.md):

• A missing solver closes the gate. With no z3 in PATH, every claim stays at e = 0. This is safe degradation by design, not a bypass.
• Debug builds are not bit-reproducible (non-deterministic DWARF in Zig 0.17). Attested artefacts are ReleaseFast.
• The static gate has ~70 % recall on the HumanEval set. It is a filter, not a prover for arbitrary code.
• proof_check.zig performs structural validation only — it is not a full Alethe/LFSC proof checker.
• The SLSA attestation is Ed25519-signed by the owner key (kern.intoto.sig, verified by python3 tools/slsa_provenance.py --check). It is not signed through a cloud Sigstore/cosign OIDC builder, so it does not claim SLSA Level 3 builder isolation.

In scope — anything that can make KERN accept what it should reject, or crash on untrusted input:

Out of scope: bugs in upstream Z3 / Lean 4 / libsqlite3 (report them upstream — but tell us if KERN's use of them is unsafe); the quality of AI models KERN checks; licence questions (see LICENSE); anything requiring a malicious local root user.

The gate is only as trustworthy as the binary you run, so this is the intended path:

curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.4.0/kernc-x86_64-linux-musl
curl -fsSLO https://github.com/newmathphys/kern/releases/download/v2.4.0/SHA256SUMS
sha256sum -c SHA256SUMS                      # must print: OK
python3 tools/slsa_provenance.py --check     # Ed25519 signature + source fingerprint

The release binary is built hermetically (zig build hermetic, static musl); the attestation binds the binary digest to the source fingerprint, and make artifact-check fails if the README, the local build and the published asset ever disagree.

For context when assessing a report:

• Merkle root over the descriptor table and SHA-256 over every payload (a one-byte modification yields PayloadTampered).
• Checked arithmetic (std.math.add/mul) on all offset and size computations.
• No @ptrCast/@alignCast in the read path — records are decoded byte-wise ([96]u8, alignment 1), which is why ARM64 reports no Bus Error.
• comptime layout assertions on every on-disk structure.
• Atomic image writes (tmp + fsync + rename + directory fsync).
• A hard timeout and FD/zombie discipline around every solver subprocess.
• Can-fail harness proving that all 81 CHECK targets are able to fail (95 non-vacuous cases, 0 vacuous, 0 case errors) — a check that cannot go red is treated as a defect here.

Thank you for helping keep KERN honest.