Theoria's trusted runtime boundary is the native kernel. Assurance commands compare that kernel with independent reference paths, re-admit checked environments through replay, and check generated artifacts. These checks improve confidence; they are not a formal proof of kernel correctness and do not imply Lean feature parity.
Main command
mix theoria.kernel.check
This runs the curated kernel corpus, generated terms, generated environment corpora, theorem-module replay, artifact replay, trusted-adjacent metadata/reduction replay, and invalid-environment rejection checks.
Useful variants:
mix theoria.kernel.check --verbose
mix theoria.kernel.check --coverage
mix theoria.kernel.check --assurance-summary
mix theoria.kernel.check --assurance-summary --coverage
mix theoria.kernel.check --json
Bounds
Generated assurance is bounded so CI remains fast:
mix theoria.kernel.check --generated-size 1 --generated-max-terms 4
mix theoria.kernel.check --environment-depth 8
Defaults are chosen for regular CI. Increase bounds locally for deeper assurance.
What the counts mean
- Curated corpus: hand-authored infer/check/normalize/defeq/rejection cases.
- Generated terms: deterministic typed terms checked against production and reference paths.
- Environment corpus: generated declaration chains replayed and normalized through production/reference paths.
- Invalid environments: malformed environments rejected with expected reason classes.
- Metadata replay: replayed declarations preserve trusted-adjacent environment metadata and reduction data. This is analogous in spirit to checking Lean environment-extension data, but it is Theoria-specific assurance, not Lean compatibility.
- Artifact replay: generated and indexed equation artifacts replay in checked environments.
Summary output
mix theoria.kernel.check --assurance-summary
prints a concise user-facing coverage summary. With --json, the output is backed by Jason-encoded structs.
Lean oracle
Contributor-only Lean validation remains separate:
mix theoria.lean.check
Lean is an external regression oracle, not part of Theoria's trusted runtime path.