Specialized Packs

khive’s default install loads nine production packs (kg, gtd, memory, brain, comm, schedule, knowledge, session, git, per RuntimeConfig::default() in crates/khive-runtime/src/config.rs). Of these, git already contributes zero verbs of its own — it registers the commit / issue / pull_request note kinds and a batch ingester for a git-lifecycle provenance graph (see crates/khive-pack-git/). Beyond the default set, khive also ships niche packs that extend the graph for a specific domain without adding verbs of their own. This guide covers the formal-math pack, the first of these, and how pack loading works in general.

Pack composition model

Every pack implements the Pack trait (crates/khive-types/) and declares, additively, what it contributes: note kinds, entity kinds, verb handlers, and edge endpoint rules. A pack can declare zero verbs and still be useful, contributing purely to the edge ontology. Packs declare a REQUIRES list of other packs that must already be loaded; the runtime resolves this at startup. See ADR-017 for the full standard, including how pack-declared edge endpoint rules combine with the base ADR-002 contract: rules are additive only, never tightening what the base contract already allows.

Loading a pack

Packs are selected via the --pack CLI flag (repeatable) or the KHIVE_PACKS environment variable (comma- or whitespace-separated):

kkernel mcp --pack kg --pack gtd --pack formal
# or
KHIVE_PACKS="kg,gtd,formal" kkernel mcp

formal declares REQUIRES = &["kg"], so kg must also be in the load set.

The formal pack

crates/khive-pack-formal/ is a pure ontology extension for formal mathematics, targeting Lean-style proof developments, built around six concept subtypes: theorem, definition, structure, instance, axiom, and goal. It is not part of the default pack set; opt in explicitly.

What it contributes

FormalPack declares:

NOTE_KINDS = &[], ENTITY_KINDS = &[], HANDLERS = &[]: no new note kinds, entity kinds, or verbs.
EDGE_RULES = &FORMAL_EDGE_RULES: 21 additive edge endpoint rules.

Every rule is expressed via EndpointKind::EntityOfType { kind: "concept", entity_type: <subtype> }: all six subtypes are concept entities distinguished by their entity_type property, not by a new EntityKind variant. Because dispatch() unconditionally returns an error naming the verb, loading formal cannot be used to call any verb. Its only effect is widening which typed edges the graph accepts.

Endpoint rules by relation

Relation	Rule count	Pairs
`depends_on`	14	theorem to {theorem, definition, structure, axiom}; definition to {definition, structure, theorem, axiom}; instance to {structure, definition}; goal to {theorem, definition, structure, axiom}
`instance_of`	1	instance to structure
`extends`	2	structure to structure; definition to definition
`variant_of`	4	theorem to theorem; definition to definition; goal to theorem; goal to definition

depends_on models the prerequisite chain, so the source uses or builds on a target: a theorem may depend on other theorems, definitions, structures, or axioms it invokes, and a goal (an unproved target) may depend on the same four subtypes it will eventually need. instance_of models an instance implementing a structure. extends models structural or definitional inheritance. variant_of models a restatement, including a goal framed as a variant of an existing theorem or definition, which is useful as an anti-duplicate signal when the same result is proposed as a fresh goal.

Example

request(ops="create(kind=\"concept\", name=\"Cauchy-Schwarz\", properties={\"entity_type\": \"theorem\"})")
request(ops="create(kind=\"concept\", name=\"Inner product space\", properties={\"entity_type\": \"structure\"})")
request(ops="link(source_id=\"<theorem_id>\", target_id=\"<structure_id>\", relation=\"depends_on\")")

With only kg loaded (no formal), the same link call is rejected. The base ADR-002 contract does not admit a concept-to-concept depends_on edge between two arbitrary subtypes on its own; the formal pack’s rules are what makes this specific (theorem, depends_on, structure) triple legal.