# Publishing guidelines

Kenton Labs · version 1.0 · 2026-10-11

## The unit of knowledge

An entry connects a precise problem, readable exposition, a formal claim,
inspectable evidence, and an explicit acceptance procedure. Define notation
before using it. Reconcile references and write a coherent line of reasoning.
Simplification must preserve the formal model. Link prerequisites, related
instances, and the sources explaining the surrounding theory.

A dataset is a family of related problems with a shared input model and task.
Publish its definitions, construction, admissible inputs, acceptance criteria,
worked instances, evidence, complexity, failure cases, and extensions. The current
22 datasets contain three worked records each. They are reference families for
exposition and reproduction, not a held-out model-evaluation benchmark.

## Exact claims

A fixed formal specification has fixed truth conditions. A problem may have
many satisfying models, equivalent programs, or equally optimal solutions.
Some formal problems are undecidable or computationally infeasible for a chosen
method. An unknown answer, timeout, or execution failure is not a negative result.
Changing arithmetic, bit width, atomicity, objective, grammar, or gate basis
changes the problem.

Keep feasibility, equivalence, soundness, safety, optimality, and performance
claims distinct. A valid candidate supplies an upper bound for minimization;
a minimum additionally requires excluding better candidates. A finite input
check does not establish an unbounded theorem. A plotted numeric approximation
is not an exact rational certificate.

## Record contract

Use a stable ID, version, area, readable question, machine-readable specification,
claim, witness or certificate, explanation, verification method and scope,
checker version, runtime, hashes, limitations, references, provenance, and human
review state. Include the family’s definitions and methodology in downloadable
record lessons. Keep JSON, Markdown, dataset downloads, and pages synchronized
through the release tool.

Record original instances separately from imported material. For an actual
machine-generation experiment, include model/build identity, prompt, seed,
parameters, budget, environment, and complete attempt logs. The current reference
corpus does not claim such an evaluation.

## Acceptance by area

| Area | Evidence required |
| --- | --- |
| Algorithms and graphs | Input contract, implementation or path, independent property/oracle, complete declared coverage or checked certificate. |
| Automata and formal languages | Alphabet, transitions or grammar, acceptance rules; product closure, membership chart, or exact bounded coverage. |
| Semantics, types, rewriting | Explicit rules and context; trace, typing reconstruction/derivation, or complete reduction closure. |
| SAT, SMT, constraints | Exact formula/theory/domain; checked model or a checked certificate/complete finite exclusion. |
| Model checking and protocols | Initial state, transition relation, property, atomicity/failure/fairness assumptions; reachability closure or replayable counterexample. |
| Abstract interpretation | Concrete and abstract semantics, sound transfer/containment evidence; distinguish a tight interval from an exact set. |
| Program verification | Preconditions, invariant, exit obligation, termination measure, and the exact checked input or state domain. |
| Circuits, scheduling, knapsack | Precise cost/resource model, feasible witness, and lower-bound or complete comparison evidence for optimality. |
| Games | Ownership and terminal rules; classify every relevant state against all opponent choices and check a strategy. |
| Information theory | Symbol probabilities, codewords, prefix/round-trip checks, exact cost; code optimality requires separate evidence. |
| Finite probability | Stochastic rows, exact recurrence or equations, horizon/target semantics; separate DTMC probability from MDP choice. |
| Relational algebra | Set/bag/NULL semantics and allowed rewrites; exact output comparison and a separate cost model. |
| GF(2) linear algebra | Field, matrix orientation, elimination or equivalent certificate, rank, and complete kernel/basis evidence. |

Custom Python checkers, finite enumeration, and exact arithmetic support the
current corpus. Future solver or proof-assistant results must identify the actual
software, proof format, trusted assumptions, and pinned dependencies. Never claim
that a source’s tool checked a Kenton artifact unless that run is recorded.

## Verification and review

Mechanical status records what the named checker actually accepted for the
exact hashed artifacts. Human review is a separate field: record reviewer,
date, scope, and decision before calling material independently reviewed.
Current records have no independent reviewer recorded. Present the knowledge
base plainly while keeping this fact available in verification metadata.

Preserve false-property results, impossibility checks, and counterexamples as
checked knowledge. Withdraw or supersede a faulty claim with a visible explanation
and a corrected version. Do not silently change an already distributed source ZIP.

## Evaluation integrity

Before using these families to evaluate a hypothesis generator, create a protocol,
baselines, resource limits, family/lineage-based splits, canonical deduplication,
and a contamination record. Keep unreleased evaluation answers separate from
public exposition. Report every attempted candidate, including failures,
timeouts, unknown results, objective gaps, and budget exhaustion. Report
uncertainty and computational resources alongside success rates.

## Graphics and publication

Interactive illustrations recompute locally and state when a control changes
the released instance. Keep a textual result and inspectable data beside the
visual. Support keyboard controls, responsive layouts, light/dark branding,
and reduced-motion preferences. Do not embed tracking or unrelated application
features in the reading experience.

Run the Python verifier, rejection suite, and browser-engine cross-checks;
build the source bundle and website; verify pages, controls, references, mobile
layout, and downloadable files. Record verification limits and hashes, preserve
prior versions, and package only the public website for Cloudflare Pages. A
prepared deployment archive is not a live deployment.

Complete every major release with the dated full-project Dropbox snapshot
required by the root AGENTS.md; verify that upload separately. Rights for original
Kenton Labs text/data/code remain undecided; source availability does not grant an
open reuse license. Record the rights of every future import before distribution.