Kalika Domain - Technical Specifications

Kalika is the implemented bounded context for scientific computation and research workflows: a Computer Algebra System (CAS), reactive research notebooks, a compute service, autonomous research agents, an SDK, a CLI, and a large body of mathematics, theoretical-physics, and materials-science kernel libraries. This document specifies the surfaces that exist in code under libs/kalika/* and apps/kalika/*. Where a capability is named in the features document but not yet built as a typed surface, it is labelled (planned).

Package Layout#

Kalika is spread across 96 TypeScript library packages, two Rust crate workspaces, a Python SDK, and 6 applications. The two Rust crates provide the high-performance kernel that all the TypeScript libraries call into.

• Libraries: @kalika/* under libs/kalika/. The repository currently carries 96 library packages plus the Rust cas-engine and numerical-engine crates and a Python SDK.
• Applications: under apps/kalika/ — bff, web, cli, svc-agents, svc-compute, svc-notebooks (6 applications).
• The foundation packages are @kalika/core (the symbolic expression model) and @kalika/utils (units, dimensions, physical constants). Every other library depends on @kalika/core.

Foundation: @kalika/core#

@kalika/core (libs/kalika/core/) defines the symbolic expression algebra, provenance model, pattern/rewrite machinery, and serialization formats. It is the canonical in-memory representation that every mathematics and physics library shares. Every expression in Kalika is an Expr value defined here; every provenance trail is a ProvenResult wrapping a value from here.

The Expr Symbolic AST#

The central type is Expr — a discriminated union over the kind field (libs/kalika/core/src/expr.ts). All nodes extend ExprNodeBase<TKind> (carrying a readonly kind); all fields are readonly, so expressions are treated as immutable values. The EXPR_KINDS tuple enumerates exactly 20 node kinds:

IntegerLiteral, RationalLiteral, RealLiteral, ComplexLiteral, Symbol, FunctionApp, BinaryOp, UnaryOp, Derivative, Integral, Sum, Product, Limit, Matrix, Tensor, Set, Piecewise, Equation, Proof, Undefined.

The table below gives the fields for each concrete node shape. Real literals are stored as strings to preserve exact decimal text, and rational/integer literals carry bigint values so that exact arithmetic is never corrupted by IEEE-754 rounding.

Enumerations on the AST#

The AST is parameterized by several closed sets of named constants. These enumerations are the typed vocabulary that all domain libraries share:

• BINARY_OPERATORS (8): +, -, *, /, ^, tensor_product, wedge_product, direct_sum. The associative operators are + and * (used by rewrite flattening).
• UNARY_OPERATORS (8): negate, conjugate, transpose, hermitian_adjoint, gradient, divergence, curl, laplacian.
• EQUATION_RELATIONS (6): =, <, >, <=, >=, !=.
• LIMIT_DIRECTIONS (5): two_sided, from_left, from_right, from_above, from_below.
• REAL_CONSTANTS (7): pi, e, sqrt2, goldenRatio, eulerMascheroniGamma, catalansConstant, aperysConstant.
• TENSOR_VARIANCES (2): covariant, contravariant. A TensorIndex is { symbol: string; variance: TensorVariance }.
• TENSOR_SYMMETRY_KINDS (3): symmetric, antisymmetric, mixed. TensorSymmetryMetadata carries kind plus indexGroups (groups of index positions sharing the symmetry).

Symbol Assumptions#

Symbols carry a SymbolAssumptions record that constrains what the symbol represents. These constraints are consulted by the simplification engine to determine when domain-specific rewrites are sound (for example, sqrt(x^2) = x is only valid when x is nonnegative). The record has four optional categories (expr.ts, assumptions.ts):

• SYMBOL_DOMAIN_ASSUMPTIONS (11): integer, rational, real, complex, positive, nonnegative, nonzero, negative, even, odd, prime.
• SYMBOL_ALGEBRAIC_PROPERTIES (8): commutative, hermitian, unitary, invertible, idempotent, nilpotent, normal, selfAdjoint.
• SYMBOL_FINITENESS_ASSUMPTIONS (3): finite, bounded, unbounded.
• predicates: readonly Expr[] — symbolic predicate facts; notes: string[].

Each category is an AssumptionTruthMap — a partial record from the assumption name to a boolean.

Assumption closure and conflict detection (assumptions.ts): analyzeSymbolAssumptions computes a SymbolAssumptionAnalysis containing the normalized assumptions (all flags filled, implications applied), a list of conflicts, and a satisfiable boolean.

Domain implications apply assumptions transitively, enabling all implied ones. The key closure rules are:

• Domain implications — integer ⇒ rational, real, complex; positive ⇒ nonnegative, nonzero, real, complex; prime ⇒ integer, positive, nonzero, rational, real, complex; even/odd ⇒ integer, ….
• Algebraic implications — hermitian ⇒ normal; unitary ⇒ invertible, normal; selfAdjoint ⇒ hermitian, normal.
• Conflicts — positive vs negative ("cannot be both strictly positive and strictly negative"); even vs odd; finite vs unbounded; bounded vs unbounded. Each conflict is a SymbolAssumptionConflict with category (domains | algebraicProperties | finiteness), assumption, conflictsWith, and a human-readable reason.

mergeSymbolAssumptions combines several assumption sets and re-runs the analysis; hasDomainAssumption / hasAlgebraicProperty / hasFinitenessAssumption answer membership after closure.

Pattern Matching and Rewrite Rules#

@kalika/core provides the rewrite engine that domain libraries extend with domain-specific rules. A RewriteRule transforms one expression into another when a pattern matches, recording why the rewrite is sound (its provenance) so the derivation chain can be verified later.

• ExprPattern (pattern.ts) — pattern AST with kinds WildcardPattern, LiteralPattern, FunctionPattern, BinaryOpPattern, UnaryOpPattern, ConditionPattern, AlternativesPattern. A WildcardPattern has a bindingName, a cardinality, and an optional constraint. analyzeExprPattern validates a pattern and reports binding info and diagnostics.
• RewriteRule (rewrite-rule.ts) — built from RewriteRuleConfig via createRewriteRule. A rule has a name, an integer priority, a provenance, a forward direction spec, and an optional reverse spec (bidirectional rules). RewriteRuleProvenance.kind is one of REWRITE_RULE_PROVENANCE_KINDS: axiom, theorem, definition, heuristic — recording why a rewrite is sound.
• REWRITE_RULE_DIRECTIONS (2): forward, reverse.
• Domain restrictions — RewriteRuleDomainRestriction gates a rule on RewriteRuleAssumptionRequirements (a symbol target plus required domain / algebraic / finiteness assumptions) and/or a predicate condition, so domain-dependent rewrites apply only when sound. Requirements target either the subject or a named binding.
• applyRewriteRule / applyRewriteRules produce RewriteRuleApplication records; applyRewriteRules sorts by compareRewriteRulePriority (descending priority, then name). Each application carries a RewriteRuleProvenanceRecord suitable for a derivation chain.

Derivations and ProvenResult#

Every non-trivial computation can carry a verifiable provenance trail. ProvenResult<T> is the central mechanism: it wraps a value of type T together with the chain of derivation steps that produced it, the assumptions consumed, and the verification status.

• DerivationStep (derivation.ts) — ruleName, inputExpr, outputExpr, optional justificationReference, an ExprPath (path), an ISO-8601 timestamp, and optional explanation. createDerivationStep rejects empty rule names and validates timestamps; derivationStepFromRewriteApplication and buildDerivationChainFromRewriteApplications lift rewrite applications into derivation chains.
• ProvenResult<T> (proven-result.ts) — wraps a value with a derivationChain: readonly DerivationStep[], an assumptionsUsed: readonly ProvenAssumption[], a confidenceLevel, and a verificationStatus.
• PROVEN_RESULT_CONFIDENCE_LEVELS (4): proven, conjectured, numerical, verified-by-independent-cas.
• PROVEN_RESULT_VERIFICATION_STATUSES (7): unverified, lean4-verified, coq-verified, smt-verified, atp-verified, numerical-spot-check, cross-cas-verified.
• ProvenAssumption is a union over PROVEN_ASSUMPTION_KINDS (symbol, predicate, note): ProvenSymbolAssumption (a symbol name plus normalized assumptions), ProvenPredicateAssumption (a predicate Expr), and ProvenNoteAssumption (a free-text note).

The following invariants are enforced by createProvenResult to prevent a heuristic or numerical result from being presented as a formal proof:

• A verification status of lean4-verified or coq-verified requires confidenceLevel === 'proven'.
• numerical-spot-check requires confidenceLevel === 'numerical'.
• cross-cas-verified requires confidenceLevel === 'verified-by-independent-cas'.
• When the confidence level is omitted, inferConfidenceLevel derives it from the verification status: formal statuses ⇒ proven; numerical-spot-check ⇒ numerical; cross-cas-verified ⇒ verified-by-independent-cas; unverified ⇒ proven if a derivation chain exists, otherwise conjectured.
• createProvenResult infers ProvenAssumptions by traversing the wrapped Expr value (collectProvenAssumptionsFromExpr) unless inferAssumptionsFromExpr is false; assumption conflicts found during traversal are recorded as note assumptions.

mapProvenResult, appendDerivationStep, and updateProvenResultVerification transform a ProvenResult while preserving its provenance.

Verification Badges#

verification-badge.ts projects verification state onto a UI badge. Badges provide a human-readable, ranked summary of how much trust to place in a computed result. The five badge levels form a strict ranking:

VERIFICATION_BADGE_LEVELS (5): formally-verified (rank 5), cross-cas-verified (rank 4), numerically-verified (rank 3), unverified (rank 1), contradiction-detected (rank 0).

Each VerificationBadge carries a level, label, description, a colors triple (background/foreground/border), and a numeric rank. verificationBadgeForStatus maps a ProvenResultVerificationStatus to a badge; verificationBadgeForComputation fuses multiple signals (formal / cross-CAS / numerical / contradiction) and returns the highest-rank badge, with any failure status forcing contradiction-detected.

Computation Result Events#

computation-result-event.ts defines an in-process event surface for completed results. This bus allows different parts of the TypeScript layer to react to computation outcomes without tight coupling.

ComputationResultEventKind (5): cas-computation, formal-verification, physics-calculation, verified-computation, custom-computation.

A ComputationResultEvent carries id, kind, sourceModule, computationType, inputExpression, outputExpression, a derivationChain, verificationStatus, optional confidenceLevel, domainTags, an ISO timestamp, and optional metadata. The ComputationResultEventBus class supports emit, subscribe, getHistory, clearHistory, and listenerCount; ids are generated as kalika:computation-event:<source>:<type>:<timestamp>:<counter>.

Serialization Formats#

@kalika/core round-trips Expr to and from several interchange formats. Multiple formats are provided because different consumers have different requirements: SMT-LIB for solver verification, TPTP for first-order ATP, OpenMath and Content MathML for interoperability with other computer algebra systems, and SCSCP for distributed CAS communication.

• serialization.ts — the native Kalika JSON encoding.
• openmath.ts — OpenMath objects (with robustness and round-trip test suites).
• content-mathml.ts — Content MathML.
• smtlib.ts — SMT-LIB (for SMT-solver verification).
• tptp.ts — TPTP (for first-order ATP verification).
• scscp.ts — SCSCP (Symbolic Computation Software Composability Protocol).
• Derivations have their own export and compression modules (derivation-export.ts, derivation-compression.ts).

Other Core Modules#

Beyond the central types and machinery, @kalika/core contains supporting modules for structural operations, compilation, and testing:

• egraph.ts — e-graph (equality-saturation) data structure with internals tests.
• hash-consing.ts — structural hashing / structuralKeyForExpr, the basis of structural deduplication and the e-graph.
• ordering.ts — a canonical term ordering for expressions.
• visitor.ts — traverseExpr, ExprPath (the address of a sub-expression).
• matching.ts — matchExprPattern, evaluateExprPredicate.
• numerical-compiler.ts — compiles an Expr to a numerical evaluator.
• differentiable-cas.ts — a differentiable CAS layer.
• metrics.ts — expression-complexity metrics.
• rewrite-strategy.ts — rewrite-strategy combinators.
• phase-113-* — adversarial-testing, performance-benchmark, and final-benchmark-report harnesses checked into the package.

Foundation: @kalika/utils#

@kalika/utils (libs/kalika/utils/) defines the units and physical-constants layer. Its purpose is to ensure that numerical results produced by the platform can always carry dimensional information — a bare number with no units is not a complete scientific result.

• dimensions.ts — physical dimensions (length, mass, time, …) and their algebra.
• physical-quantity.ts — a value tagged with a unit/dimension.
• physical-constants.ts and the generated physical-constants.generated.ts — codified physical constants.

This package backs the Scientific Reproducibility requirement that numerical results carry units.

CAS Kernel: @kalika/cas-engine#

@kalika/cas-engine (libs/kalika/cas-engine/) is a Rust workspace — the performance-critical symbolic-manipulation kernel — not a TypeScript package. The kernel runs in Rust for speed and correctness guarantees; the TypeScript layer calls it through either the native Node binding (for server-side use) or the WebAssembly build (for browser and SDK use).

The workspace comprises three crates:

• kalika-cas-core — the kernel itself. It implements:
  • expr — the Rust Expr mirror, canonicalization, e-graph equality saturation, JSON/binary/LaTeX serialization.
  • integer / rational / modular / padic / algebraic / ball — exact and certified arithmetic: arbitrary-precision integers, rationals, modular arithmetic, p-adics, algebraic numbers, and interval "ball" arithmetic.
  • polynomial / sparse_polynomial — polynomial algebra.
  • calculus — differentiation, the Risch transcendental and algebraic-extension integration algorithms, Rubi rule-based and heuristic integration, Gruntz limits, series expansion, symbolic summation (Gosper, Zeilberger, creative telescoping, WZ certificates), and symbolic ODE/PDE classification and solving.
• kalika-cas-native — a napi-rs native Node.js binding exposing KalikaCasNativeKernel. Bridge methods include: roundTripExpressionJson, canonicalizeExpressionJson, simplifyExpressionJson, differentiateExpressionJson, the Risch / Rubi / heuristic integration bridges, gruntzLimitExpressionJson, seriesExpandExpressionJson, zeilbergerSumExpressionJson / gosperSumExpressionJson / creativeTelescopingExpressionJson, batch variants, zero-copy buffer helpers, and worker-thread dispatchParallelChecksum / dispatchStreamingCanonicalizeJson. It advertises NAPI version 8 and a NativeBridgeCapabilities record.
• kalika-cas-wasm — a wasm-bindgen WebAssembly build exposing KalikaCasWasmKernel, with the JSON-bridge equivalents of the kernel operations plus JsValue-based roundTripExpr / canonicalizeExpr.

The cas-engine project.json defines Cargo-based Nx targets. The available build targets are: build, build:native (via scripts/build-native.sh), build:wasm (via scripts/build-wasm.sh), test (cargo test --workspace), typecheck (cargo check), typecheck:wasm (the wasm32-unknown-unknown target), lint (cargo fmt --check), and Criterion bench:* targets for integer arithmetic, polynomial algebra, and symbolic integration. The kernel ships test suites for limit regression, published integration suites, Risch decidability, simplification regression, and a differential-equation benchmark.

Numerical Kernel: @kalika/numerical-engine#

@kalika/numerical-engine (libs/kalika/numerical-engine/) is a Rust crate workspace (kalika-numerical-engine-core) with its own Cargo manifest and rust-toolchain.toml. It is the foundation for numerical workloads; the bulk of its solver surface is planned (see Planned Capability Libraries).

SDK: @kalika/sdk#

@kalika/sdk (libs/kalika/sdk/) is the embeddable client library, intended for external applications that want Kalika computation without deploying the full service stack. The KalikaSdk class wraps a WASM-local CAS so that a browser or Node.js application can run symbolic operations entirely in-process.

The SDK exposes the following methods:

• Symbolic methods — symbolic(operation, request), plus the convenience wrappers simplify, differentiate, integrate, solve, series, limit. SymbolicOperation is simplify | differentiate | integrate | solve | series | limit.
• evaluate — numeric evaluation of an expression with a variable map.
• matrix(operation, request) — MatrixOperation is add | subtract | multiply | transpose | determinant | inverse | trace.
• tensor(operation, request) — TensorOperation is einsum | shape.
• execute(job) and batch(jobs) — run a ComputeJob or an array of jobs (a ComputeJob is a discriminated union over kind: symbolic, evaluate, matrix, tensor).
• physics — a PhysicsUtilities bundle: oscillatorEnergy, deBroglieWavelength, relativisticEnergy, schwarzschildRadius, planckLength, plus a PHYSICAL_CONSTANTS table (speed of light, reduced and full Planck constant, gravitational constant, elementary charge, Boltzmann constant).

Every SDK result is a ComputeResponse<T> (ok: true, result, metadata). ComputeMetadata records operation, engine, durationMs, verificationStatus (proven | numerical | conjectured), a verificationBadge level, the full verificationBadgeDetails, and executionMode: 'wasm-local'. createKalikaSdk constructs the SDK over a WasmArithmeticKernel.

@kalika/sdk-python is a separate Python SDK package under libs/kalika/sdk-python/.

Research Notebooks: @kalika/notebooks#

@kalika/notebooks (libs/kalika/notebooks/) defines the reactive notebook document model and execution engine. The central design decisions are immutability of cell content (editing a cell resets its execution state and clears outputs) and reactivity (cells that depend on upstream results are automatically re-evaluated in topological order rather than document order).

Notebook Document Model (model.ts)#

The document model defines the structure of a notebook on disk and in memory:

• NotebookDocument — format (always the constant kalika.notebook), formatVersion (always 1), id, title, optional description, cells: readonly NotebookCell[], and metadata.
• NotebookDocumentMetadata — createdAt, lastModified (ISO-8601 timestamps), tags: readonly string[], optional authors, optional kernel, optional custom JSON object.
• NotebookCell — id, type, content (string source), execution, outputs: readonly NotebookOutput[], executionCount: number | null, and metadata (createdAt, lastModified, tags, optional language, title, custom).
• NOTEBOOK_CELL_TYPES (5): code, markdown, latex-math, visualization, prose.
• NotebookCellExecution — status plus optional startedAt, completedAt, durationMs, and error.
• NOTEBOOK_EXECUTION_STATUSES (4): idle, running, completed, errored. Invariant: an errored execution must carry an error payload (name, message, optional stack), and only an errored execution may carry one.
• NOTEBOOK_OUTPUT_TYPES (8): text, latex, html, svg, image, data-table, interactive-widget, custom. Each output type has a fixed MIME type — text/plain, text/latex, text/html, image/svg+xml, image/*, application/vnd.kalika.table+json, application/vnd.kalika.widget+json, and an arbitrary MIME for custom. normalizeOutput enforces the MIME contract (e.g. a data-table row length must equal the column count; an image encoding must be base64 or url).
• The notebook text file extension is .kalika-nb.

Document invariants (normalizeNotebookDocument): the format and format version must match the constants; id and title must be non-empty; cell ids must be unique; executionCount (when not null) must be a non-negative integer. addNotebookCell, removeNotebookCell, moveNotebookCell, updateNotebookCellContent, replaceNotebookCellOutputs, and markNotebookCellExecution are immutable transforms that touch metadata.lastModified. Editing a cell's content resets its execution to idle and clears outputs.

Reactive Execution Engine (reactive-engine.ts)#

The reactive engine is what makes a Kalika notebook different from a simple script runner. It analyzes which cells define which variables and which cells consume them, builds a dependency graph, and plans a topological execution order. When a cell changes, only the affected downstream cells are re-evaluated.

• NotebookCellExecutionMode (cell-mode.ts) — reactive or mutable.
• analyzeNotebookCellVariables extracts the variables a cell defines and reads; analyzeTypeScriptVariables and analyzeMathVariables are the per-language analyzers.
• buildNotebookDependencyGraph produces a NotebookDependencyGraph of NotebookDependencyEdges and NotebookReactiveDiagnostics.
• planReactiveExecution / planIncrementalReactiveExecution produce a ReactiveExecutionPlan — the topological execution order, which can differ from document order; detectNotebookCellSymbolChanges and collectAffectedCells drive incremental re-evaluation when an upstream cell changes; executeReactivePlan runs the plan with a ReactiveCellExecutor.

Other Notebook Modules#

The notebook package includes a number of supporting modules beyond the core document model and reactive engine:

• cas-kernel.ts — the CAS kernel binding used by math cells.
• cell-execution.ts — cell-execution mechanics.
• collaboration.ts — multi-user collaboration state (NotebookCollaborationEdit, NotebookCollaboratorPresence, locks).
• comments.ts — notebook comments.
• dependency-locking.ts — dependency-graph locking.
• citations.ts / citation-suggestions.ts — citation management and suggestion.
• provenance.ts — notebook provenance records.
• reproducibility.ts — NotebookExecutionReproducibilityOptions, NotebookRandomSeedRecord (NotebookReproducibilitySeedSource), NotebookExecutionEnvironmentRecord, and NotebookSystemArchitectureRecord. Metadata key kalika.reproducibility, schema version 1.
• environment-metadata.ts — NotebookEnvironmentSpecification, NotebookEnvironmentDependency, NotebookEnvironmentDependencyLockSummary. Metadata key kalika.environment, schema version 1.
• reproducible-export.ts — reproducible export bundles.
• Interop / format modules — serialization.ts (native JSON), plain-text.ts, jupyter-interoperability.ts (.ipynb), mathematica-notebook.ts, pluto-notebook.ts, latex-paper-import.ts.
• output-rendering.ts — output rendering helpers.
• assistant.ts — notebook AI assistant.
• sharing.ts / versioning.ts — notebook sharing and version history.
• domain-physics-templates.ts and ising-notebook-paper.ts — prebuilt physics notebook templates and a worked Ising-model paper notebook.

Research Agents: @kalika/research-agents#

@kalika/research-agents (libs/kalika/research-agents/) implements the autonomous-research substrate. The key design principle is that Kalika owns scientific semantics (what a conjecture, proof, or experiment campaign means) while consuming generic agent machinery from Nous. This separation ensures that improvements to Kalika's scientific domain model benefit all agent types, without requiring Kalika to maintain its own agent scheduling, evaluation harnesses, or model serving.

Research Agent Base (research-agent-base.ts)#

A research run is planned and executed step-by-step, with the agent reflecting on its own progress between iterations. The base structures that all agents share are:

• ResearchGoalSpecification — question plus optional formalConstraints (Expr | string), assumptions, domain, acceptanceCriteria, expectedOutputs, metadata.
• ResearchPlanStep — id, kind, objective, description, dependsOn, requiredToolKinds, status, attempts, diagnostics, artifactIds.
• ResearchPlanStepKind (7): scope, compute, literature, verify, reflect, synthesize, custom.
• ResearchPlanStepStatus (5): pending, running, completed, failed, blocked.
• ResearchToolKind (6): cas, literature, formal-verification, reflection, reporting, custom.
• ResearchArtifactKind (8): goal, computation, literature, proof, counterexample, reflection, report, note. A ResearchArtifact carries id, kind, stepId, title, content, optional confidence, citations, provenResults, and metadata.
• ResearchReflection — iteration, progressScore, completedStepIds, deadEnds, adjustments, nextActions, diagnostics.
• ResearchReport — title, summary, findings, proofs, citations, openQuestions, markdown.
• ResearchAgentRun — id, agentId, status (ResearchAgentRunStatus: completed | partial | failed), goal, plan, artifacts, reflections, report, diagnostics, startedAt, completedAt. ResearchAgentBase defaults to 12 iterations and 1 retry per step.

Proof Agent (proof-agent.ts)#

The proof agent attempts to formally verify or disprove a mathematical conjecture by trying a sequence of methods in order of increasing sophistication. The agent short-circuits as soon as it finds a proof or disproof.

• ProofConjecture — statement (Expr | string), optional description, leanContext, computationTasks, metadata.
• ProofAgentStatus (4): proved, disproved, inconclusive, not-run.
• ProofAgentMethod (6): decision-procedure, smt, atp, lean-proof-search, lean-tactic, computation.
• The agent runs computations first; a numerically-failed computation short-circuits to disproved. It then tries (in order, where enabled) a built-in decision procedure, an SMT solver, a first-order ATP, Lean proof-tree search (searchLeanProofTree), and Lean tactic prediction (predictAndAttemptLeanTactics) — each producing an AutomatedReasoningAttempt. A natural-language statement with no formal Expr cannot reach the formal methods. The verifiers come from @kalika/formal-verification.
• ProofAgentResult — status, conjecture, optional method, optional proof (proof text), counterexamples, computations, attempts, diagnostics.

Conjecture Formulation (conjecture-formulation.ts)#

The conjecture formulation module is responsible for proposing new mathematical statements worth investigating. A formulated conjecture is ranked on four axes to prioritize which conjectures to attempt first.

• FormulatedConjecture — id, sourcePatternId, sourcePatternKind, naturalLanguage, formalStatement: Expr, conditions, conclusion, supportObjectIds, ranking, counterexampleSearch, diagnostics.
• ConjectureRanking — novelty, plausibility, significance, falsifiability, and an overall score, plus impliedBy (KnownTheoremReference[]) and a rationale.
• CounterexampleSearchPlan — strategy, targetVariables, suggestedObjectFamilies, and a priority of low | normal | high.

Multi-Agent Orchestrator (multi-agent-orchestrator.ts)#

The orchestrator coordinates multiple specialist agents — each focused on one aspect of a research goal — and merges their outputs into a unified research run. Specialist tasks are organized as a dependency graph so that, for example, the synthesis agent only runs after the literature and computation agents have completed.

• MultiAgentResearchRequest extends ResearchGoalSpecification with optional computationTasks, literatureQuery, explorationTarget, proofConjectures, the include* flags, and metadata.
• MultiAgentSpecialistKind (6): scope, literature, computation, exploration, proof, synthesis.
• MultiAgentTaskStatus (5): pending, running, completed, failed, blocked.
• MultiAgentRunStatus (3): completed, partial, failed.
• A MultiAgentTask carries id, kind, objective, dependsOn, status, attempts, optional input, optional result, artifactIds, diagnostics. The orchestrator plans a dependency graph of specialist tasks and produces a MultiAgentResearchRun (tasks, dependencyGraph, artifacts, report, diagnostics, startedAt, completedAt).

Specialist Agents and Integrations#

The research agent package bundles a set of specialist agent implementations and integrations with external scientific literature sources:

• computation-agent.ts — ComputationAgent, ComputationTask, ComputationAgentResult (CAS computation with verification).
• exploration-agent.ts — ExplorationAgent, ExplorationTarget, ExplorationReport.
• literature-agent.ts — LiteratureAgent, LiteratureSearchQuery.
• Literature clients — arxiv-client.ts, inspire-hep-client.ts, openalex-client.ts, semantic-scholar-client.ts, oeis-integration.ts.
• Proof tooling — proof-search-tree.ts, proof-repair.ts, tactic-prediction.ts, retrieval-augmented-proving.ts.
• Conjecture tooling — pattern-detection-engine.ts (DetectedPattern, PatternDetectionResult), funsearch-conjecture-generation.ts, batch-conjecture-testing.ts, conjecture-validation-pipeline.ts, conjecture-generation-benchmarks.ts.
• Paper verification — paper-claim-verification.ts, paper-reproduction.ts, derivation-comparison.ts, errata-detection.ts.
• agent-memory.ts — agent memory; computation-receipt.ts — computation receipts.
• human-in-the-loop.ts — human-review gating.
• nous-integration.ts — integration with the Nous autonomous-research substrate (Nous supplies the generic agent machinery; Kalika keeps the scientific semantics).

Application: BFF (apps/kalika/bff)#

apps/kalika/bff is a Fastify backend-for-frontend (@kalika/bff, version 0.1.0) composing the three downstream services for the web workbench. The BFF is the only service the browser talks to directly; it authenticates the caller, fans requests to the appropriate downstream services, and fans real-time events back over WebSocket.

Authentication#

createKalikaAuthHook requires a bearer token on every route except /health, /ready, and the /api/v1/ws/* WebSocket routes. Two token kinds are accepted (KalikaAuthContext.tokenKind):

• dev tokens (dev.<base64url-json>, allowed only when NODE_ENV !== 'production' or allowDevTokens).
• jwt tokens (HS256, verified by @oshun/auth's JwtService; default issuer kalika-bff, audience kalika-web).

The auth context carries userId, role (UserRole: anonymous, user, premium, creator, moderator, admin, super_admin; below user is rejected), scopes (default kalika:read, kalika:write), permissions (role permissions from getPermissions merged with explicit ones), sessionId, and expiresAt.

HTTP Routes#

All non-WebSocket routes are under /api/v1. Responses use the { ok: true, result } / { ok: false, error } envelope.

bodyLimit is 8 MiB. CORS allows GET,POST,PUT,PATCH,DELETE,OPTIONS and the headers content-type,authorization,x-request-id, x-kalika-client. Upstream failures surface as KALIKA_UPSTREAM_ERROR (502 for upstream 5xx); unknown routes return KALIKA_BFF_ROUTE_NOT_FOUND.

Sessions and Preferences#

KalikaSessionRecord holds id, userId, createdAt, lastSeenAt, and preferences. KalikaUserPreferences are theme (system | light | dark), computeMode (auto | browser-wasm | remote), optional defaultNotebookId, citationStyle (aps | apa | mla | chicago), realtimeChannels, and updatedAt. The default store is InMemoryKalikaSessionStore.

Realtime Hub#

KalikaRealtimeHub manages WebSocket connections, fanning BFF-side events to the relevant per-user connections. RealtimeChannel is the template type `compute${string}` | `notebook:${string}` | `agent:${string}`. A connection with the kalika:realtime scope is auto-subscribed to compute, notebook:*, and agent:*. publishToUser fans an event to a user's matching connections; a RealtimeEvent carries id, type, userId, channel, payload, createdAt. BFF routes publish realtime events on queue submission/cancellation (compute.queue.submitted, compute.queue.cancelled), cell/notebook execution (notebook.cell.execution.queued, notebook.execution.queued), and agent activity (agent.run.started, agent.research-task.created).

Application: Compute Service (apps/kalika/svc-compute)#

apps/kalika/svc-compute (@kalika/svc-compute) is the Fastify compute service. It handles both synchronous computation requests (symbolic, numerical, matrix, tensor) and longer asynchronous workloads via its BullMQ-backed queue. bodyLimit is 4 MiB.

HTTP Routes#

Request and Response Types#

The compute service speaks a uniform request/response protocol over all operation types. Errors are always structured (ComputeErrorResponse) rather than HTTP error status codes alone.

• SymbolicRequest — expression, optional variable, order, point, around, terms.
• EvaluationRequest — expression, optional variables map.
• MatrixRequest — optional left, right, matrix (row-major numeric matrices).
• TensorRequest — optional einsum expression plus tensors (each a TensorDescriptor with data, shape, optional labels).
• ComputeResponse<T> — { ok: true, result, metadata } with ComputeMetadata (operation, engine, durationMs, verificationStatus of proven | numerical | conjectured). Errors are ComputeErrorResponse ({ ok: false, error: { code, message } }).
• ComputeJob — discriminated union over kind: symbolic (with a SymbolicOperation), evaluate, matrix (with a MatrixOperation), tensor (with a TensorOperation). BatchRequest wraps jobs; BatchResponse.jobs are BatchItemResults (fulfilled | rejected).

Operation Enumerations#

These closed enumerations define exactly which operations the compute service accepts. New operations require extending the enum and the corresponding handler.

• SymbolicOperation (6): simplify, differentiate, integrate, solve, series, limit.
• MatrixOperation (7): add, subtract, multiply, transpose, determinant, inverse, trace.
• TensorOperation (2): einsum, shape. The compute engine uses @kalika/tensor-networks for einsum/tensor.
• StreamingOperation (3): groebner_basis, large_simplification, numerical_simulation.

Streaming Computations#

The /api/v1/ws/stream socket runs long-running operations where progress reporting and early cancellation matter. A StreamStartMessage carries the operation and a typed payload (GroebnerBasisStreamRequest, LargeSimplificationStreamRequest, or NumericalSimulationStreamRequest); a StreamCancelMessage aborts by id. StreamServerEvent kinds: stream.started, stream.progress, stream.partial, stream.completed, stream.cancelled, stream.error — each carries a StreamProgress (phase, completed, total, percentage) where applicable.

Compute Queue#

The queue (queue.ts) is built on BullMQ and handles workloads that are too expensive for synchronous HTTP. The default backend is memory; the alternative is redis, selected by KALIKA_COMPUTE_QUEUE_BACKEND=redis with KALIKA_COMPUTE_QUEUE_REDIS_URL.

• QueueSubmitRequest — task: QueuedComputeTask, optional priority, timeoutMs, idempotencyKey.
• QueuedComputeTask — discriminated union over kind: compute (a ComputeJob), ibp_reduction (an IbpReductionRequest — integration-by-parts reduction of Feynman integrals), lattice_monte_carlo (a LatticeMonteCarloRequest — a 2-D Ising-style Monte Carlo sweep).
• ComputeQueuePriority (3): interactive (weight 1), batch (5), background (10). Higher weight means lower priority in the BullMQ scheduler.
• ComputeQueueStatus (6): queued, running, completed, failed, cancelled, timed_out.
• QueueJobRecord — jobId, status, priority, task, timeoutMs, cacheKey, cacheHit, submittedAt, optional startedAt, completedAt, progress, result, error. Identical tasks share a content-hashed cacheKey, so a repeated submission can be served from cache (cacheHit).
• ComputeQueueStats — backend (memory | redis), the per-status counts, cacheEntries, and workerCount. The default worker count is 2 and default timeout 30 s; both are overridable via KALIKA_COMPUTE_QUEUE_WORKERS and KALIKA_COMPUTE_QUEUE_TIMEOUT_MS.

Configuration#

The compute service reads the following environment variables: KALIKA_COMPUTE_QUEUE_BACKEND, KALIKA_COMPUTE_QUEUE_REDIS_URL, KALIKA_COMPUTE_QUEUE_WORKERS, KALIKA_COMPUTE_QUEUE_TIMEOUT_MS, NODE_ENV.

Application: Notebook Service (apps/kalika/svc-notebooks)#

apps/kalika/svc-notebooks (@kalika/svc-notebooks) is the Fastify notebook execution and storage service. It hydrates a NotebookService on startup and is responsible for cell and notebook lifecycle, collaboration state, and file-sync with the local filesystem. bodyLimit is 8 MiB.

HTTP Routes#

Service Types#

The notebook service introduces several types for execution jobs, export formats, file synchronization, and collaboration state:

• NotebookExecutionJob — id, notebookId, cellId, status, submittedAt, optional startedAt/completedAt/durationMs/ language, diagnostics, prerequisiteJobIds, optional error.
• NotebookExecutionJobStatus (5): queued, running, completed, failed, cancelled.
• ExecuteNotebookCellRequest.language (4): typescript, cas, python, lean4.
• NotebookExportFormat (7): json, html, latex, pdf, ipynb, plain, kalika. A NotebookExportResult carries format, filename, contentType, and a body. (The BFF's parseNotebookExportFormat accepts the first six; the notebook service additionally accepts kalika.)
• NotebookKernelState — executionCount, optional resetAt, variables.
• NotebookFileSyncStatus — notebookId, state (unbound | binding | watching | error), optional path, a revision counter, and the last-synced/written/external-change timestamps. NotebookFileSyncMode is auto | load | save; NotebookFileSyncEvent types are bound, saved, external-change, error, unbound, snapshot.
• Collaboration requests cover edits, raw CRDT updates (updateBase64), presence, and lock acquisition/release (CollaborationLockRequest carries a cellId, userId, optional displayName, reason, ttlMs, lockId, metadata).

Application: Agent Service (apps/kalika/svc-agents)#

apps/kalika/svc-agents (@kalika/svc-agents) is the Fastify research-agent lifecycle service. It hosts a ResearchAgentLifecycleService and manages the full lifecycle of managed agents — creation, resource provisioning, running, pausing, resuming, termination — plus research task submission and human feedback collection. bodyLimit is 2 MiB.

HTTP Routes#

Agent Lifecycle Types#

The agent service introduces a set of types for tracking agent identity, resource consumption, run history, and human oversight:

• ManagedAgentKind — multi-agent.
• ManagedAgentStatus (4): idle, running, paused, terminated.
• ManagedRunStatus (4): running, completed, failed, cancelled.
• ManagedAgentRecord — id, kind, ownerId, label, status, resources, createdAt, updatedAt, optional activeRunId, runIds, and lifecycleEvents.
• AgentLifecycleEvent.type (6): created, run_started, run_completed, paused, resumed, terminated.
• AgentResourceRequest / AgentResourceLease — a Claude API key (stored only as a fingerprint), a computeBudgetMs, a tokenBudget, and metadata.
• AgentCostEstimate — estimated and reserved Claude prompt/completion tokens, estimated compute ms, estimated USD, token and compute budgets, used and remaining amounts, a withinBudget flag, and budgetViolations.
• AgentUsageRecord — per-owner accumulated Claude tokens, compute ms, estimated USD, and runIds.
• ManagedRunRecord — id, agentId, status, submittedAt, optional startedAt/completedAt, the request (a MultiAgentResearchRequest or a plain string), optional result (MultiAgentResearchRun), optional error, optional usage, and feedback.
• HumanFeedbackRecord — id, runId, createdAt, optional reviewerId, a note, an optional verdict (approve | revise | reject), and metadata.
• ResearchTaskView / IntermediateResultsView / FinalReportView — the read-model projections returned by the research-task endpoints, carrying progress (completedTasks / totalTasks / percentage), artifacts, tasks, citations, proofs, and feedback.

Application: Web Workbench (apps/kalika/web)#

apps/kalika/web is the React research-workbench application. It is the human-facing surface of the platform — where researchers author notebooks, submit computations, explore results spatially, collaborate in real time, and publish findings. Modules under web/src/ implement these surfaces:

• math-input.ts — direct mathematical-notation entry feeding the CAS.
• spatial-canvas.ts — a non-linear spatial workspace alongside the linear notebook.
• ThreeDExplorer.tsx / three-d-explorer.ts — 3-D visualization.
• inline-animation.ts — inline animations driven by computed results.
• declarative-diagram.ts — declarative diagram rendering.
• accessible-math.ts — accessible mathematics rendering; the workbench carries an accessibility audit (e2e/accessibility-audit.spec.ts, phase-113-accessibility-compliance.spec.ts).
• research-assistant.ts / ai-suggestions.ts — the in-workbench AI assistant and inline suggestions.
• citation-sidebar.ts — the citation sidebar.
• knowledge-graph-browser.ts — the knowledge-graph browser.
• realtime-collaboration.ts — collaborative editing.
• proof-exploration.ts — interactive proof exploration.
• shareable-computation-links.ts — shareable computation links.
• state-transition.ts — workbench state-machine transitions.
• Workflow modules — compute-verify-workflow.ts, compute-write-workflow.ts, explore-conjecture-workflow.ts, literature-informed-workflow.ts, paper-generation-workflow.ts, theory-observable-workflow.ts — the end-to-end research workflows that string together computation, verification, literature search, and publication.

Playwright e2e specs cover the notebook UI and accessibility compliance.

Application: CLI (apps/kalika/cli)#

apps/kalika/cli (@kalika/cli) is the kalika command-line tool. It runs over the @kalika/sdk WASM CAS, so all symbolic operations execute locally without a running server. The available commands are:

• kalika eval <expression> [--var name=value] [--json] — evaluate or run a CAS call (simplify, differentiate/diff, integrate, solve, series, limit).
• kalika simplify <expression>, kalika solve <equation> [--var-symbol x] — direct symbolic operations.
• kalika notebook run <file.kalika-nb|file.kalika> — execute a notebook file's non-prose cells.
• kalika training-data <subcommand> — delegates to @kalika/training-data: ingest-proof-pile, ingest-formal-proofs, ingest-arxiv-latex, download-arxiv-latex, ingest-structured-db, generate-synthetic, train-math-classifier, score-quality, train-quality-model, dedupe-training-data, balance-domains. These ingest and curate scientific training corpora (Proof-Pile, Lean4/Mathlib, Coq/MathComp, Isabelle/AFP, Metamath, arXiv LaTeX, LMFDB, OEIS, the Stacks Project, KnotInfo/LinkInfo, the PDG, …).

Mathematics, Physics, and Materials Libraries#

Beyond the foundation, the compute kernels, the research substrate, and the research-platform packages, libs/kalika/ carries an extensive set of domain libraries. Each extends the @kalika/core symbolic AST with domain objects and adds domain-specific rewrite rules, algorithms, and tests. These are real, substantive TypeScript packages (most carry 5–40 source modules); the implementation depth varies by package.

Pure Mathematics#

The 27 pure mathematics packages cover the major branches of modern mathematics. @kalika/calculus and @kalika/differential-geometry are thin façade packages that name @kalika/cas-engine as their backend — they enumerate the CAS capabilities they front (e.g. @kalika/calculus exports CALCULUS_CAS_ENGINE_CAPABILITIES: symbolic differentiation, symbolic integration, limits, series expansion, symbolic ODE solving) — with the heavy algorithms living in the Rust kernel.

@kalika/algebra, @kalika/algebraic-combinatorics, @kalika/algebraic-geometry, @kalika/analysis, @kalika/approximation, @kalika/arithmetic, @kalika/calculus, @kalika/category-theory, @kalika/cohomology, @kalika/combinatorics, @kalika/differential-geometry, @kalika/geometric-analysis, @kalika/higher-categories, @kalika/measure-theory, @kalika/noncommutative-geometry, @kalika/number-theory, @kalika/optimal-transport, @kalika/optimization, @kalika/periods, @kalika/positive-geometry, @kalika/probability, @kalika/quantum-groups, @kalika/symplectic, @kalika/three-manifolds, @kalika/topology, @kalika/tropical, @kalika/vertex-algebras.

Theoretical and Continuum Physics#

The physics packages cover the major frameworks from classical to frontier physics. Theoretical astrophysics and mathematical-physics tooling live here; observatory and astronomy calculations belong to Nyx, not Kalika.

@kalika/astrophysics, @kalika/atomic-physics, @kalika/bbn (Big Bang nucleosynthesis), @kalika/bootstrap (conformal bootstrap), @kalika/classical-mechanics, @kalika/condensed-matter, @kalika/cosmology, @kalika/electrodynamics, @kalika/entanglement, @kalika/feynman, @kalika/fluid-dynamics, @kalika/general-relativity, @kalika/gravitational-waves, @kalika/hep-phenomenology, @kalika/information-theory, @kalika/integrable-systems, @kalika/lattice (lattice field theory), @kalika/lie-theory, @kalika/mathematical-physics, @kalika/matrix-models, @kalika/neutrino-physics, @kalika/non-perturbative, @kalika/nonlinear-dynamics, @kalika/open-quantum-systems, @kalika/optics, @kalika/particles, @kalika/plasma-physics, @kalika/quantum-chaos, @kalika/quantum-computing, @kalika/quantum-field-theory, @kalika/quantum-gravity, @kalika/quantum-mechanics, @kalika/resurgence, @kalika/spectral-geometry, @kalika/statistical-mechanics, @kalika/string-theory, @kalika/supersymmetry, @kalika/tensor, @kalika/tensor-networks, @kalika/thermodynamics, @kalika/topological-qc.

Numerical and Compute#

Numerical packages bridge the Rust kernel to TypeScript orchestration, and provide higher-level numerical methods on top of it. ODE/PDE solvers, Monte Carlo methods, GPU acceleration, and special-function numerics named in the features document are (planned) extensions of numerical-engine.

@kalika/numerical, @kalika/autodiff, @kalika/autodiff-core, @kalika/hpc-orchestrator, @kalika/sdp-core (semidefinite programming), @kalika/surrogate, plus the Rust @kalika/numerical-engine and @kalika/cas-engine crates.

Formal Verification and ML for Science#

Formal verification packages connect the symbolic kernel to automated theorem-proving systems, enabling the lean4-verified, coq-verified, smt-verified, and atp-verified verification statuses.

• @kalika/formal-verification — a Lean bridge, decision procedures, SMT-solver and first-order-ATP verification: decideWithBuiltInProcedure, verifyWithSmtSolver, verifyWithFirstOrderAtp, LeanReplSession.
• @kalika/symbolic-regression — symbolic regression.
• @kalika/neural-physics — physics-informed neural networks.
• @kalika/training-data — the Phase 108 ML-sovereignty surface. Beyond scientific-corpus ingestion and curation (Proof-Pile, formal proofs, arXiv LaTeX, structured databases, synthetic data, quality scoring, deduplication, domain balancing — the CLI subcommands above), the package implements: embedding-model training — math-similarity training configs (math-embedding-training.ts), LaTeX-aware preprocessing with separate natural-language and mathematical-content channels (preprocessLatexForEmbedding, canonicalizeLatexForEmbedding), and Lean proof-state premise-retrieval datasets, training jobs, and evaluation (buildProofStateEmbeddingDataset, createProofStateEmbeddingTrainingJob, evaluateProofStateEmbeddingModel); custom-model training pipelines — math tokenizer extension, continued pretraining, instruction-tuning datasets, mathematical constitutional AI, math-domain reward models, RLVF, CAS-in-the-loop training, and hybrid-reasoning and tool-use fine-tuning; the data flywheel — ComputationResultEventBus/knowledge-graph integration, flywheel metrics, targeted synthetic data, model A/B testing, and a weekly model refresh with skipped/deployed/rolled_back outcomes; serving and routing — an intent-based serving router (KalikaServingRouterRequest) across direct-cas, fast-7b, balanced-34b-tools, frontier-72b-search, and lean-mcts targets, multi-size model routing, prefix KV caching, and speculative decoding; and math benchmarks (kalika-math-benchmark.ts, external-benchmark-evaluation.ts).

Materials Science (electronic structure)#

The three built materials packages implement the most compute-intensive first-principles method at the core of modern materials science.

• @kalika/electronic-structure — Kohn-Sham DFT with a plane-wave basis, pseudopotentials, the SCF solver, band structure, density of states, and related outputs.
• @kalika/xc-functionals — exchange-correlation functionals.
• @kalika/wannier — Wannier functions.

The broader materials program — crystallography, many-body methods, lattice dynamics, molecular dynamics, ML potentials, defects/surfaces/interfaces, transport and other properties, spectroscopy, thermodynamics and phase diagrams, functional materials, code interoperability (VASP, Quantum ESPRESSO, ABINIT, LAMMPS, …), and multiscale engineering — is (planned) (features document, Phases 116–131).

Autonomous Experimentation (planned)#

Closed-loop discovery — experiment orchestration, design of experiments, robotic protocols, instrument and beamline control, an ExperimentCampaign unit of physical-lab work, lab-safety and human-governance checkpoints — is a (planned) program (features document, Phase 130). The ExperimentCampaignUpdated event named in the features document is part of this planned surface.

Research Platform#

The research platform packages provide the output layer — turning computed results into human-readable, citable, and reproducible research artifacts.

@kalika/notebooks, @kalika/renderer, @kalika/typesetting (LaTeX / mathematical typesetting), @kalika/knowledge-graph (the scientific knowledge graph of mathematical objects, papers, methods, hypotheses, and materials facts), @kalika/citations, @kalika/database, and the @kalika/jupyter-kernel package directory.

Events#

Implemented event surface#

Kalika's implemented events are in-process and WebSocket/SSE, not a cross-domain message bus. The following event channels are live today:

• ComputationResultEvent (@kalika/core) — emitted on a ComputationResultEventBus for completed computations; kinds cas-computation, formal-verification, physics-calculation, verified-computation, custom-computation.
• BFF realtime events — the BFF publishes compute.queue.submitted, compute.queue.cancelled, notebook.cell.execution.queued, notebook.execution.queued, agent.run.started, and agent.research-task.created to per-user WebSocket channels via KalikaRealtimeHub.
• Compute streaming events — stream.started, stream.progress, stream.partial, stream.completed, stream.cancelled, stream.error over the compute service's stream socket.
• Notebook file-sync events — bound, saved, external-change, error, unbound, snapshot over the notebook service's SSE stream.
• Agent lifecycle events — recorded on each ManagedAgentRecord: created, run_started, run_completed, paused, resumed, terminated.

Planned event surface#

The features and architecture documents describe a domain-level event surface that would allow other domains to subscribe to Kalika computation outcomes without polling. That cross-domain bus integration is (planned); the implemented surface today is the in-process and WebSocket/SSE eventing above. The planned events are:

ExpressionEvaluated, NotebookCellExecuted, ComputeJobSubmitted, ComputeJobCompleted, ProofAttemptCompleted, ArtifactRegistered, ResearchFindingPublished, ExperimentCampaignUpdated.

Persistence#

The implemented services use in-memory stores by default — InMemoryKalikaSessionStore (BFF sessions), the NotebookService repository (hydrated on startup), and the ResearchAgentLifecycleService store. The compute queue persists either in memory or, when configured, in Redis (BullMQ).

A durable PostgreSQL store for projects, notebooks, job records, citations, and collaboration state, and an object/artifact store for datasets, environment bundles, replay bundles, rendered media, and provenance records, are the (planned) persistence layer described in the architecture document.

Scientific Reproducibility Contract#

Reproducibility is a cross-cutting correctness contract enforced across the domain. It is implemented through a chain of interlocking mechanisms rather than a single check, so that a result cannot lose its provenance at any layer.

• Verifiable provenance — ProvenResult<T> (@kalika/core) attaches a derivationChain, assumptionsUsed, a confidenceLevel, and a verificationStatus to a computed value. The status invariants (formal statuses require proven; numerical-spot-check requires numerical; cross-cas-verified requires verified-by-independent-cas) prevent a heuristic or numerical result from being presented as a formal proof.
• Proof status — the proof agent (ProofAgentStatus: proved, disproved, inconclusive, not-run) and @kalika/formal-verification always report which method (decision-procedure, smt, atp, lean-proof-search, lean-tactic, computation) produced an outcome.
• Verification badges — VerificationBadgeLevel projects verification state for the UI; contradiction-detected is rank 0, so a rejected or counterexampled result can never display above an unverified one.
• Units — @kalika/utils carries dimensions, physical quantities, and codified physical constants so numerical results can be units-tagged.
• Notebook reproducibility — @kalika/notebooks captures random seeds (NotebookRandomSeedRecord, NotebookReproducibilitySeedSource), the execution environment (NotebookExecutionEnvironmentRecord, NotebookSystemArchitectureRecord), and dependency locks (NotebookEnvironmentDependencyLockSummary) under the kalika.reproducibility and kalika.environment metadata keys (schema version 1), and supports reproducible export bundles.
• Compute reproducibility — queued compute jobs content-hash their tasks into a cacheKey, so an identical re-submission yields an identical (cache-served) result.
• Kernel verification — the Rust CAS kernel ships regression and benchmark suites (limit regression, published integration suites, Risch decidability, simplification regression, the differential-equation benchmark, and Criterion micro-benchmarks); @kalika/core carries adversarial-testing and performance-benchmark harnesses.

Cross-Domain Boundaries#

These boundaries exist to prevent duplication and keep responsibilities clear. Each line below states both the ownership split and why the boundary is drawn where it is.

• Sophia owns general knowledge management and RAG; Kalika owns the scientific knowledge graph (@kalika/knowledge-graph). The boundary separates general document retrieval (Sophia's concern) from the structured, typed graph of mathematical objects, proofs, and physical constants (Kalika's concern).
• Nous owns generic AI model infrastructure and the autonomous-research substrate; @kalika/research-agents consumes Nous via nous-integration.ts while keeping the scientific (conjecture / proof / campaign) semantics in Kalika. The boundary ensures that Nous can improve its agent scheduling and model serving without coupling to Kalika's domain model, and vice versa.
• Nyx owns astronomy and observatory calculations; Kalika keeps theoretical astrophysics and mathematical-physics tooling. The boundary is the telescope: theoretical calculation is Kalika's; interfacing with a real instrument or sky survey is Nyx's.
• Iris supplies assistant and conversational interfaces consumed by the Kalika workbench.
• Saraswati, Brigid, Cybele, Airmid, Demeter, Maat consume validated scientific and materials outputs for technology, manufacturing, construction, botanical, agriculture, and planning workflows without owning the scientific kernels. The boundary exists so that kernel improvements benefit all consumers simultaneously.