The trusted core of the toolchain. A Calculus of Constructions type checker, written in pure Rust, that re-checks every proof the rest of the stack proposes. Trust stops there. Everything above it gets re-checked.
Most of the stack is allowed to be wrong. The parser, the proof search, the arithmetic normalizer, the English front end: none of them are trusted, and none of them can make something true by asserting it. They propose. The kernel disposes.
What sits at the bottom is a type checker for the Calculus of Constructions, CIC flavored, with inductive types, fixpoints and pattern matching. Prop is impredicative and universes are cumulative. Terms, types and proofs are one syntactic category, so checking a proof and checking a type are the same operation.
That is the whole trick, and it's why the compiler's output is worth believing. A proof about your silicon is only as good as the thing that checked it, so the thing that checks it stays small, pure Rust, and re-runs from scratch every time.
The kernel is not one algorithm. Search proposes a derivation, and the checker re-verifies it, and in between sit the procedures that decide the goal in the first place. The SAT solver is one of them.
| Layer | Purpose |
|---|---|
| Type checkinginfer_type, is_subtype, normalize | Bidirectional inference over the Calculus of Constructions, cumulative subtyping, and normalization. Terms, types and proofs are one syntactic category. |
| Soundness gatespositivity, termination | Strict positivity, which rejects the inductive definitions that would encode Russell's paradox, and a syntactic termination guard that rejects fixpoints which never stop. |
| Decision proceduresring, lia, omega, cc, simp, bitvector | Polynomial equalities, linear inequalities by Fourier Motzkin over the rationals, exact integer arithmetic, congruence closure over uninterpreted functions, rewriting, and bit-permutation identities. |
| SAT and model checkingcdcl, sat, twosat, hornsat, bmc, dimacs | A CDCL core with 2-watched literals, 1-UIP learning and VSIDS, plus the specialists that beat it on structure: 2-SAT, Horn-SAT, and bounded model checking. This is the one people mean by the solver. |
| Algebraic proof systemsxorsat, modp, polycalc, pseudo_boolean, sos | Gaussian elimination over GF(2) and GF(p), Nullstellensatz and polynomial calculus, cutting planes, and exact sum of squares. These are different proof systems, not a faster search. |
| Symmetrysymmetry_detect, sym_break, sym_certify, permgroup | Detection, lex-leader breaking, certified breaking, and the non-abelian coset decision by Schreier Sims. Symmetry is why the pigeonhole family below finishes at all. |
| Certificatescertificate, recheck | A proof term, its claimed type, and a prelude version, serialized as JSON. Re-checkable by anyone who trusts none of our code. |
Trust runs in one direction across all of it, from fast to strong. An untrusted CDCL or SMT run gets you an answer quickly. A RUP certified refutation gets you an answer an independent checker has already confirmed. A kernel certified proof gets you a term the type checker accepted against the goal. Anything that fails to certify comes back unverified. It never comes back true.
The trusted computing base is the kernel type checker plus seven commutative ring axioms for primitive integer arithmetic. That is the entire inventory, and a test holds it there, so the trusted base cannot grow without the build failing. Closed arithmetic needs none of them: 2 + 3 = 5 is proven by computation.
A certificate carries three things. The proof term, the claimed type, and a prelude version. It never carries a context. The re-checker rebuilds the trusted axiom set itself and then requires the term's inferred type to be a subtype of the claim, so a certificate cannot arrive carrying its own permission to be true. That is the De Bruijn criterion, and the trusted surface of a re-check is the kernel crate and a JSON parser. No proof search. No SMT.
Z3 sits outside the trusted base, along with the proof search, the arithmetic normalizer and the English front end. Anything the SMT oracle finds is elaborated into a kernel checked proof rather than taken on faith, and it appears here as a benchmark comparator and in two optional crates left out of the default build. There are also goals the oracle declines and the kernel certifies by structural induction, because induction is not something an SMT solver does.
cargo run -p logicaffeine-kernel --example recheck --features serde -- cert.jsonRun that against any certificate we produce. The checker is small enough to audit by hand, which is the only reason a claim about a trusted base means anything.
Certain obligations that come out of hardware verification are unreachable for the solvers most toolchains ship. Symmetry between identical units, counting arguments over a resource, and parity constraints across a datapath all produce formulas that a resolution based solver cannot finish at realistic sizes. Not slowly. At any size, because a lower bound proved by Haken in 1985 says no short proof exists in that system.
An engineer meeting one of these does not see a proof system boundary. They see a run that never returns, and they fall back to simulation and a coverage argument. This prover exists so that class of obligation has an answer instead of a workaround.
Different algebra, same philosophy
There is no single trick here. Each family is decided by the structure it actually contains: symmetry, matching, linear algebra over a field or a ring, or the ordering itself. The mechanism is named alongside every result, because a time without a mechanism reads as tuning.
Byte identical DIMACS to every solver. Median of five runs. Timeouts of 10 s for Z3, 15 s for Kissat, CaDiCaL and CryptoMiniSat, and 45 s for SaDiCaL so the PR solver runs to completion. Intel Core i9-14900K, Kissat 4.0.4, CaDiCaL 3.0.0, CryptoMiniSat 5.11.21.
| Family | Ours | The field |
|---|---|---|
| Pigeonhole, 16 holesCertified SR symmetry breaking | 13.7 ms, 25 KB | SaDiCaL 56.5 ms at 242 KB. Z3, Kissat, CaDiCaL, CryptoMiniSat do not finish |
| Pigeonhole, 40 holesCertified SR symmetry breaking | 1389 ms, 513 KB | SaDiCaL 6504 ms at 25.1 MB. The resolution solvers do not finish |
| Mutilated chessboard, 18 by 18Maximum matching, Hall witness | 225 µs, 1 KB | Z3, Kissat, SaDiCaL, CaDiCaL, CryptoMiniSat all do not finish |
| Tseitin parity on an expander, n = 110Gaussian elimination over GF(2) | 18 µs | SaDiCaL 11.8 s at 7.0 MB. Z3, Kissat, CaDiCaL do not finish |
| Tseitin on a bounded treewidth grid, n = 160Gaussian elimination over GF(2) | 3.1 ms, 8 KB | Every other solver does not finish, though a short proof is known to exist |
| Mod 7 Tseitin, n = 20Gaussian elimination over GF(7) | 17 µs | Kissat 5851 ms at 35.9 MB. A GF(2) engine returns the wrong answer entirely |
| Linear ordering GT(40)Ordering specialist | 5.9 ms, 6 KB | Kissat 48.3 ms. SaDiCaL and Z3 do not finish |
The families above carry structure a resolution solver cannot exploit: symmetry between identical units, counting arguments over a resource, and parity. The kernel decides them in a proof system built for that structure, and every verdict comes back as a certificate that is re-checked rather than as a trusted answer from the solver that produced it.
Source: Every family, every size, and the full methodology, logicaffeine.com(opens in a new tab)
It runs the same in a browser as in continuous integration, because it is pure Rust with no external runtime to install. Certificates are JSON, so a party who trusts none of our code can re-check them. The crates are on crates.io and the command line is largo.
How does a prover like this fit into verifying silicon?