v1.9

Bounded improvement protocols

TensorLang is a good abstraction for bounded, inspectable AI improvement workflows: it makes artifacts, metrics, search spaces, eval suites, effects, gates, and loop bounds explicit. It is not an unrestricted recursive-self-improvement runtime.

examples/40_bounded_trace_improvement.tltensorlang
(module examples.bounded_trace_improvement
  (tensorlang "1.9")

  (artifact base_trace_model
    (kind model)
    (schema trace-classifier-v1)
    (hash "sha256:...")
    (source "build/artifacts/base-trace-model.json"))

  (artifact improved_trace_model
    (kind model)
    (schema trace-classifier-v1)
    (hash "sha256:...")
    (source "build/artifacts/improved-trace-model.json"))

  (artifact trace_dataset_v3
    (kind dataset)
    (schema semantic-traces-v1)
    (hash "sha256:...")
    (source "build/datasets/semantic-traces-v3.json")
    (split train validation test))

  (metric validation_f1
    (type F64)
    (source trace_eval)
    (direction maximize))

  (objective improve_trace_classifier
    (maximize validation_f1)
    (subject-to (>= validation_f1 0.92)))

  (search-space trace_model_search
    (choice embedding_dim [16 32 64])
    (choice learning_rate [0.1 0.03 0.01]))

  (eval-suite trace_eval
    (dataset trace_dataset_v3)
    (holdout test)
    (metrics validation_f1)
    (seed 1337)
    (deterministic true))

  (candidate trace_model_candidate
    (parent base_trace_model)
    (search-space trace_model_search)
    (produces improved_trace_model)
    (changes embedding_dim learning_rate))

  (effect train_model
    (reads base_trace_model trace_dataset_v3)
    (writes improved_trace_model)
    (network false)
    (max-cpu-seconds 600)
    (max-memory-mb 4096))

  (gate promote_trace_model
    (candidate trace_model_candidate)
    (requires (> validation_f1 parent.validation_f1))
    (requires (>= validation_f1 0.92))
    (requires (approval human)))

  (improvement-loop trace_classifier_loop
    (start base_trace_model)
    (candidate trace_model_candidate)
    (evaluate trace_eval)
    (promote-if promote_trace_model)
    (effects train_model)
    (max-iterations 5)
    (rollback-on regression)
    (emit-trace true)))
v1.9 protocol commandstensorlang
tl check examples/40_bounded_trace_improvement.tl --static-only

tl improvement-ledger   examples/40_bounded_trace_improvement.tl   trace_classifier_loop

tl check examples/41_bad_unapproved_promotion.tl   --static-only   --json
protocol

Artifacts

Immutable models, datasets, programs, eval reports, checkpoints, traces, and ledgers are named with schema, source, and hash metadata.

protocol

Objectives

Metrics declare type, source, and direction; objectives separate optimization targets from promotion constraints.

protocol

Search spaces

Candidate generation is finite and typed, with checker errors when a candidate changes knobs outside the declared space.

protocol

Eval suites

Heldout splits, metric lists, seeds, and determinism are explicit instead of hidden in orchestration code.

protocol

Effects

External runtimes must declare reads, writes, network policy, CPU/memory/step budgets, and determinism expectations.

protocol

Promotion gates

A successor is not accepted merely because it exists; gates record metric thresholds, regression checks, and approval requirements.

safety boundary

v1.9 validates and records a protocol; it does not autonomously invent objectives, rewrite source, call tools, train at scale, deploy, or promote successors. The ledger is a deterministic audit skeleton for an external governed runtime, with human or policy approval represented as an explicit gate requirement.

Apple reference

Pure Swift TensorLang checker

The native Apple implementation is canonical source in the parent TensorLang repo at apple/TensorLang. The web site documents it; the web repo does not own, vendor, or duplicate the Swift package.

what it is

TensorLangKit is a Foundation-only Swift Package Manager library target intended for macOS, iOS, iPadOS, tvOS, watchOS, and visionOS apps. The package also ships a native Swift tlexecutable target for developer workstations and CI.

Current scope is the TensorLang v0.3 checker/conformance subset. That makes it a portable Apple reference and compatibility target, but not yet a complete Swift port of every Python v2.0 runtime feature.

Package
apple/TensorLang/Package.swift
Library
apple/TensorLang/Sources/TensorLangKit
DocC
apple/TensorLang/Sources/TensorLangKit/TensorLangKit.docc
CLI
apple/TensorLang/Sources/tl/main.swift
Examples
apple/TensorLang/Examples/*.tl
App examples
apple/TensorLang/Examples/AppIntegration
SwiftUI sample
apple/TensorLang/Samples/SwiftUIApp
Golden JSON
apple/TensorLang/Conformance/examples-v0.3.project.json
Regeneration
apple/TensorLang/Scripts/check-apple-reference.sh
Lean sidecar
formal/Lean
Ownership doc
docs/APPLE_SWIFT.md
Swift and Lean verificationshell
# canonical source lives in the parent TensorLang repo
cd apple/TensorLang

swift test
swift build -c release
Scripts/check-apple-reference.sh

.build/release/tl check Examples/*.tl
.build/release/tl check --json Examples/markov_chain.tl

# formal sidecar, when Lean is installed
cd ../../formal/Lean
lake build
implemented checker coverage
  • Foundation-only TensorLangKit library target for Apple app targets
  • tl developer CLI target for checking and JSON conformance output
  • S-expression lexer and parser
  • Import-aware multi-file project checker when all sources are supplied
  • Domain size and label validation
  • DType validation for Bool, I64, F32, F64, Int, Float, Real, Nat, and Prob
  • Rank-1 and rank-2 tensor data checks
  • Bool, integer, natural, and probability cell validation
  • row-sum-eq constraint checking for probability-style rows
  • Shape inference for einsum, or, min, add, tanh, slice, and sum
  • Fixpoint initialization and step shape validation
  • Recurrent state initialization and step shape validation
  • DocC package documentation and copy-in app integration examples
boundary
  • The parent repo owns the Swift and Lean source; web only documents it.
  • The Swift checker is v0.3-subset conformance, not full Python v2.0 runtime parity.
  • The Lean sidecar is a formal scaffold, not the Apple runtime.
  • Apps link TensorLangKit; the CLI is developer tooling.
Use TensorLangKit in an appswift
import TensorLangKit

let result = TensorLang.check(sourceText, file: "EditorBuffer.tl")

for diagnostic in result.diagnostics {
    print(diagnostic.formatted())
}

let project = TensorLang.checkProject([
    SourceFile(path: "family.tl", text: familySource),
    SourceFile(path: "ancestor.tl", text: ancestorSource),
])
App model patternswift
import Combine
import Foundation
import TensorLangKit

@MainActor
final class TensorLangDocumentChecker: ObservableObject {
    @Published private(set) var diagnostics: [Diagnostic] = []
    @Published private(set) var modules: [CheckResult] = []

    func check(source: String, fileName: String) {
        let result = TensorLang.check(source, file: fileName)
        diagnostics = result.diagnostics
        modules = [result]
    }
}
real app setup
1 · Add package

After cloning the parent repo, add apple/TensorLang as a local Swift package in Xcode.

2 · Link product

Link the TensorLangKit product to the app target; do not ship the CLI.

3 · Check source

Run TensorLang.check for one document or checkProject for imports.

4 · Display issues

Bind Diagnostic values to an issue list, use formatted() for logs, and jump by line/column.

Direction

Roadmap

Cards tagged done are implemented in the current repository. v2.0 moves the previous production research items into scoped, test-covered reference capabilities.

v0.9 — done
  • ·Beyond LLM demos
  • ·Benchmark reports
  • ·Semantic traces
  • ·KG training demo
v1.0 — done
  • ·Trainable tensor programs
  • ·Model artifacts
  • ·Trace classifier
  • ·Reservoir readout
v1.1 — done
  • ·In-memory relational backend
  • ·SQLite reference backend
  • ·SQL emission
  • ·Autodiff graph inspection
v1.2 — done
  • ·Evidence suite
  • ·Evidence artifacts
  • ·Suite traces
  • ·Claim caveats
v1.3 — done
  • ·Trace world model
  • ·OpenTelemetry fixture
  • ·C-MAPSS fixture
  • ·FB15k-237 fixture
foundation slice — done
  • ·Character tokenizer
  • ·Tiny causal LM
  • ·Foundation artifacts
  • ·Autoregressive generation
v1.4 — done
  • ·Tiny transformer block
  • ·Sharded checkpoint manifests
  • ·Finite proof certificates
  • ·Energy measurement harness
v1.5 — done
  • ·Named-axis einsum
  • ·Sparse COO tensors
  • ·Join/project
  • ·Gather and scatter-add
v1.6 — done
  • ·Datalog export
  • ·TypeDB export
  • ·Relational export CLI
  • ·Conformance fixtures
v1.7 — done
  • ·Generic autodiff graph
  • ·Gradient reference metadata
  • ·Generic Adam
  • ·Structured graph metadata
v1.8 — done
  • ·Tiny-transformer reverse-mode
  • ·Accelerator lowering artifacts
  • ·Distributed optimizer manifests
  • ·Finite proof-calculus reports
v1.9 — done
  • ·Artifacts and objectives
  • ·Search spaces and candidates
  • ·Eval suites and gates
  • ·Effects and ledger CLI
v2.0 — done
  • ·Production pretraining plans
  • ·Executable accelerator runtime
  • ·Multi-process local training
  • ·Theorem-prover CLI
Apple reference — done
  • ·TensorLangKit Swift package
  • ·Native tl checker
  • ·Conformance JSON
  • ·Lean sidecar scaffold
Interop

Relationship to Capsulang

Capsulang is a sibling research language — unrelated to any existing product of that name — that explores capsule-based reasoning orchestration on top of a tensor-equation core like TensorLang.

TensorLang provides
The tensor-equation core
  • Named-axis tensors over pluggable semirings
  • Fixpoints, joins, gather/scatter, autodiff
  • Reasoner manifests and verification obligations
Capsulang orchestrates
Capsule-level reasoning
  • Composing reasoners into capsules and dialogues
  • Goal scheduling, evidence routing, control flow
  • Consuming TensorLang manifests as a runtime
+----------------+        manifest         +-----------------+
|  Capsulang     |  <-------------------   |   TensorLang    |
|  reasoner      |   tensors / domains /   |   core runtime  |
|  orchestrator  |   semirings / proofs    |                 |
+----------------+                         +-----------------+
Get involved

Contributing & research status

TensorLang is an early research prototype. Issues, design notes, and small reproducible programs are the most useful contributions right now.

How to report issues
  1. Reproduce against the current README, SPEC.md, and CLI tl --version output; when possible, also try the in-browser playground.
  2. Minimise to a single .tl module — keep domains small (size ≤ 4) so finite verification stays cheap.
  3. Include the expected vs. observed diagnostic, the CLI command, and the toolchain version printed by tl --version.
  4. File under one of: parser, checker, semiring, verify, dynamics, backend, export, or spec.
  5. Security-sensitive reports (sandbox escape from export backends, SMT panics on adversarial input) should be marked private.
good first issues
additional dtype coercion tests · playground keyboard shortcuts · example programs for new semirings · spec typo fixes
active
Tensor-logic conformance

Add fixtures that compare named-axis semiring-einsum, explicit join/project, sparse COO materialization, and relational backend output.

active
Backend conformance

Grow fixtures beyond the v1.6 baseline that compare reference, in-memory, SQLite, Datalog text, and TypeDB text without claiming formal backend proof.

active
Finite verification

Expand the SMT lowering for Bool/Nat tensors, add bounded model-checking for fixed-point reachability, and surface counter-models in the CLI.

next
Dynamics layer

Stabilise the discrete and explicit-Euler step semantics, add symplectic and implicit integrators, and standardise trace export for offline analysis.

next
Foundation model path

Move from the tiny causal LM to transformer blocks, reverse-mode autodiff lowering, tokenizer/dataset pipelines, and sharded checkpoints.

next
Backend adapters

Broaden SQL, Datalog, TypeDB, JAX, and PyTorch integrations around small, stable IR contracts, with external validators remaining optional.

research
Probabilistic semirings

Carrier laws, normalisation, and interaction with fixpoints. Open questions around inference vs. simulation duality.

research
Differentiable fragment

Identify the largest sub-language with well-defined gradients across semirings; relate to existing autodiff IRs.

What's next — verification
  • · Counter-model rendering in the playground (highlight failing cells).
  • · SMT export hardening for Nat and bounded Int.
  • · Lean obligation shape stabilisation for fixed points.
  • · Property DSL: (assert (forall …)) sugar over current primitives.
What's next — dynamics
  • · Implicit and symplectic integrators alongside explicit Euler.
  • · Stable trace format (NDJSON) for offline plotting and diffing.
  • · Step-level invariants checked during simulation, not only at the boundary.
  • · Recurrent-network reference lowering shared with the differentiable fragment.
Sister project. Capsulang explores a complementary capsule-based interop layer that TensorLang targets via its capsulang manifest.
Visit capsulang.com →
Get started

Try the reference toolchain

The reference implementation ships as a small CLI and a library. Programs are .tl S-expression files; the toolchain provides parsing, type checking, sparse COO materialization, named-axis einsum, semiring lowering, finite verification, backend execution, structured training, evidence reports, fixture-backed datasets, foundation-model training/generation, and simulation.

tensorlang-spec-v0.3.pdf · legacy v0.3 static snapshot. Current functionality is documented on this page, in README.md, and in SPEC.md.
archived tensorlang-examples-v0.3.zip
  • README.md — run/export guide
  • family.tl — finite domain + relation
  • ancestor.tl — fixpoint, OrAnd
  • shortest_path.tl — MinPlus semiring
  • reachability.tl — Boolean closure
  • markov_chain.tl — Prob, row-stochastic
  • linear_solve.tl — Real einsum
  • reservoir.tl — recurrent dynamics
  • verify_demo.tl — assert + SMT

Released under CC0 as an archived starter bundle. For current coverage, use the repository examples and the CLI commands on this page.

quick starttensorlang
; 1. check the v1.8 tensor-logic, relational, autodiff, and lowering path
tl check examples/32_tensor_logic_primitives.tl
tl lower-relalg examples/32_tensor_logic_primitives.tl user_role_action
tl emit-datalog examples/29_rel_backend_policy.tl can_do
tl lower-autodiff examples/17_training_linear_regression.tl fit
tl lower-accelerator examples/17_training_linear_regression.tl mse --target gpu
tl run-accelerator examples/17_training_linear_regression.tl mse --target numpy

; 2. validate a bounded improvement protocol
tl check examples/40_bounded_trace_improvement.tl --static-only
tl improvement-ledger examples/40_bounded_trace_improvement.tl trace_classifier_loop

; 3. run the evidence suite
tl evidence-suite --out build/evidence --quick --json

; 4. train a structured tensor model
tl train examples/26_kg_link_prediction_train.tl fit \
  --backend auto \
  --save-artifact build/kg_model.tla.json \
  --json

; 5. train and sample the tiny foundation LM
tl foundation-train \
  --text "tensorlang trains local language models." \
  --steps 80 \
  --save-artifact build/foundation.tlf.json \
  --json
tl foundation-generate \
  --artifact build/foundation.tlf.json \
  --prompt tensorlang \
  --tokens 32 \
  --json
tl foundation-optimizer-state \
  --artifact build/foundation.tlf.json \
  --out build/foundation.optimizer.json \
  --ranks 2

; 6. run v2.0 production capability surfaces
tl foundation-pretrain-plan \
  --layers 24 \
  --heads 16 \
  --model-dim 2048 \
  --ff-dim 8192 \
  --training-tokens 10000000000 \
  --json
tl foundation-distributed-train \
  --text "tensorlang synchronizes gradients." \
  --workers 2 \
  --steps 2 \
  --json
tl theorem-prove examples/43_theorem_prover_family.tl

; 7. run executable backend, proof, and foundation checks
tl rel-compare examples/30_rel_backend_reachability.tl reachable --json
tl proof-calculus examples/11_properties_family.tl
tl benchmark foundation-lm --json