logos
λόγοςReasoning that never asks to be trusted — every conclusion arrives with an account anyone can re-check.
reasoning — works out what follows, as accounts you can re-check
https://github.com/Bitspark/logos ↗Why it exists
If ontos is what is, logos is the account of what is. The problem it owns is reasoning you don't have to take on faith. A bare answer is a claim — you either trust whoever produced it or you don't. logos deals in something stronger: an account, a structured, re-checkable record of why something holds. Its single rule is conclude nothing you cannot show.
The key move is that reasoning runs in two directions over one shared artifact. Search finds an account that establishes an answer — untrusted, free to use any strategy. Check verifies an account someone already produced, without redoing the search — cheap, total, trusting nothing about where it came from. What a searcher produces is exactly what a checker consumes.
A concrete example
An account is a small positive proof DAG — a Derivation of three node kinds: a Rule (a clause instance with premises), a Builtin (an atom some theory decides, like arithmetic or comparison), and a Leaf (an extensional fact admitted by a verifier). A Rule might conclude permit(s1, a1) from a positive premise resolving to the fact grant(s1, a1) and a negated premise \+ denied(s1, a1) — discharged not by a node but by that atom's genuine absence from a sealed closed-model certificate the derivation cites.
A query doesn't name an engine; it states a RequiredProfile — what the answer must be worth across semantics, representation, guarantee, and answer shape. A three-stage resolver negotiates which engine answers. One of four — relational, seminaive, sldnf, wam — searches and emits a candidate. Then the certify gate, the sole minter of a certificate, re-runs a search-free check() and admits the result only if it holds.
What it unlocks
logos reasons over the shared beings ontos defines, adding the one notion being doesn't need: the unknown. With a published checker contract and the dual-conformance law — every emitted answer must carry a derivation the checker accepts — other systems can build on the checking direction. thesmos, the admission law — who may — is its first consumer on the demanding side: its rule is to check a supplied account, never to go searching. Further up the spine, stele (the public record) builds on the same published checker contract. See where it all sits in the stack.
What's next
The account grammar is FIRM and the checker SPI is STABLE-v1 (additive-only), both accepted; the certifying portfolio kernel is built and running. The four-engine portfolio itself stays proposed — strategies may still change behind the frozen seam — with cross-engine agreement and dual-conformance held by the conformance harness. The roadmap lives in the repo's own plans; see the decisions for why each seam sits where it does.
Depended on by
codes to logos's published checker SPI (logos-contract): admit = check, gate = solve + check over thesmos's law
intent — the tri-core certifying kernel links logos's check/solve implementation; today only logos-contract is pinned in the manifests
codes to logos's published checker SPI (logos-contract — the Derivation/checker types), not logos's engine; the authorization program logos checks
the tri-core compiles/links logos's checker package — cli/{go,rs} + core/{go,rs} pin github.com/Bitspark/logos/contract/go and the logos-contract git dep; today only logos-contract is compiled, not the engine
implements logos's published checker SPI (Theory / LeafVerifier / RuleAdmissibility) and supplies a typing Program logos checks; consumes check(), never searches
drives logos as a benchmark subject — the CLI/in-process seam plus the vendored substrate BOM snapshot it resolves release ids from; a downstream consumer only, logos never depends on logos-bench
the benchmark reads against logos's published CLI surface (ADR 0015) and kernel/contract SPI, not its internals
the reasoning layer's published contract (github.com/Bitspark/logos/contract/go) — predicates, rules and the eligibility vocabulary prism authors against
the Go backend links the logos KERNEL too (github.com/Bitspark/logos/kernel/go) — certify/outcome/runtime/seam/wasm, not just the contract, so prism evaluates rules in-process rather than describing them
codes to logos's published checker SPI (logos-contract) — the seam reuses logos-contract types verbatim (Symbol/GroundLiteral/Derivation/Evidence/Theory/Clause/ClauseId/Goal + CheckProfile), pinned per-language in seam/{go,rs,ts} (contract/go v0.9.1, logos-contract git tag v0.9.1, @bitspark/logos-contract 0.9.1)
the certify spine it wraps and hosts — logos check()/solve (contract + kernel); SearchAndCertify = search-for-a-derivation → check(), so every certified answer is a logos derivation. Intent — the engine links logos's check/solve implementation; today only logos-contract is pinned in the seam manifests
builds to the logos contract — go dep github.com/Bitspark/logos/contract/go v0.9.1
Examples involving logos
A worked walkthrough of one protected action — admitting a signed fact — as a gate whose account any party can re-check.
A walkthrough of one participant becoming usable by another written years later, through substrate-visible evidence alone — and where that story is realized today versus still a sketch.
Docs exported by logos
docs entry ↗docs/architecture/kernel.md
docs/spec/logos-contract.md
docs/architecture/decisions/README.md