ZTARE 0.1.0
First tagged public release of ZTARE — a zero-trust research engine that keeps neural proposers strictly separate from deterministic verifiers, gates, and append-only ledgers, so the model cannot self-certify. The discipline is the product: it improves research rigor; it does not guarantee truth.
Highlights
- leanmill — governed Lean proof-search engine: a governed DAG search over a typed move algebra behind a single anti-laundering kernel (axiom allowlist + statement-integrity + MNC) with composite decomposition→closure ratification. The solver proposes; governance ratifies. Environment lift is measured, not assumed (lift-pending).
- Autoresearch law-discovery factory (
discover → compress → prove) with the symbolic fitter, holdout tests, and Lean kernel as the only arbiters. - Shared
common/libraries: sandboxed execution, symbolic-witness / SymPy compute, constraint isomorphism, and more — reused across both lanes. - Primitive registry + atlas with an amnesia precheck to reuse capabilities before building new ones.
- Deterministic publish-safety and anti-gaming gates, each dogfooded so it cannot silently rot.
- Public analytics dashboard (GitHub Pages), leak-masked.
Full notes: see CHANGELOG.md.