Unit tests check 3 points. SMT proves the entire 2^64 space.
I built KERN (Zero-Trust L0-L5 verification gateway in Zig 0.17 + Z3):
https://github.com/newmathphys/kern
Tired of green CI pipelines passing buggy code, we ran our solver against real open-source repos:
1. TheAlgorithms/C (catalan.c):
factorial(0) returned 0 instead of 1 -> division by zero SIGFPE on n=0, and silent overflow from n=11.
PR: TheAlgorithms/C#1595
2. TheAlgorithms/Rust (binomial_coefficient.rs):
n - i underflowed u64 when k > n -> panic in debug, silent garbage in release.
PR: TheAlgorithms/Rust#1075 (Codecov 100% patch coverage)
3. EvalPlus MBPP+:
Found 3 unhandled ZeroDivisionErrors in code that passed 80 unit tests.
Now shipping v2.8.0:
- Native Zig AST verifier built directly into the static kernc binary (0 Python, 0 regexes).
- Evaluated against official SMT-LIB and SV-COMP benchmarks.
- 180/180 non-vacuous can-fail checks, sealed with Ed25519 attestations.
Stop trusting "1 passed in 0.01s". Verify ∀x.GitHubGitHub - newmathphys/kern: Zero-trust L0-L5 verification gateway in Zig 0.17: native Z3 proof-DAG checker, Belnap B4 logic, 42 Lean 4 theorems (0 sorry), 8-lane SIMD BLAKE3 (.kimg) & MCP server.Zero-trust L0-L5 verification gateway in Zig 0.17: native Z3 proof-DAG checker, Belnap B4 logic, 42 Lean 4 theorems (0 sorry), 8-lane SIMD BLAKE3 (.kimg) & MCP server. - newmathphys/kern
commit cb4f6f9