TensorLang is experimental, so this page puts status, examples, benchmarks, evidence artifacts, and verification hooks in one place. The goal is to make capability claims reproducible and caveated.
TensorLang is an experimental reference implementation. The point of this section is to be transparent about what exists today versus what is staged research.
(semiring plus-times (type F64) (zero 0.0) (one 1.0) (add +) (mul *)) (def similarity (type F64) (shape Doc Doc) (expr (einsum "Left Feature, Right Feature -> Left Right" doc_feature doc_feature)))
(property no_self_ancestor (forall ((x Person)) (not (at ancestor x x)))) ; CLI: ; tl verify examples/11_properties_family.tl --json ; tl emit-smt examples/11_properties_family.tl ; tl emit-lean examples/11_properties_family.tl
Benchmark reports measure local wall-clock and CPU time, estimate peak memory with tracemalloc, record correctness metrics, and state clearly that no external LLM call was made.
tl benchmark policy-closure --json tl benchmark requirement-coverage --json tl benchmark trace-root-cause --json tl benchmark dynamic-anomaly --json tl benchmark kg-link-prediction --json tl benchmark kg-training --json tl benchmark trace-classifier-training --json tl benchmark reservoir-readout-training --json tl benchmark rel-policy-inmem --json tl benchmark rel-policy-sqlite --json tl benchmark rel-reachability-inmem --json tl benchmark rel-reachability-sqlite --json tl benchmark autodiff-kg-training --json tl benchmark foundation-lm --json tl benchmark policy-closure --json --trace-jsonl /tmp/tensorlang-trace.jsonl
TensorLang now bundles its strongest demos into one evidence suite: finite reasoning, requirement coverage, semantic trace root-cause analysis, dynamic anomaly detection, structured training, executable relational backends, and autodiff evidence.
Policy closure and requirement coverage run as deterministic tensor/relation programs, with finite Boolean verification where applicable.
Semantic trace fields become data that can be reasoned over, producing causal paths instead of prose-only log summaries.
KG, trace-classifier, reservoir-readout, and foundation-LM demos train explicit local models and emit reusable artifacts.
Relational targets can be compared across reference, in-memory, and SQLite backends; autodiff lowering is inspected where available.
The suite writes evidence.json, evidence_summary.json, EVIDENCE.md, per-case traces, and model artifacts.
No LLM calls, no energy measurement claims, and no formal proof claims for learned numeric outputs.
tl evidence-cases tl evidence-suite --out build/evidence --quick --json tl evidence-suite --out build/evidence --size small
evidence.json — full machine-readable reportevidence_summary.json — compact web/dashboard summaryEVIDENCE.md — generated human-readable reportsuite.trace.jsonl and traces/*.jsonl — semantic trace evidenceartifacts/*.json — generated model artifactsThe evidence suite does not try to make TensorLang compete with LLMs at language. It demonstrates the complementary cases where explicit local tensor/relation/dynamics programs are more repeatable, checkable, and inspectable than repeated probabilistic text inference.
Verification today is finite-model exhaustive checking with hooks to export obligations. It is not a full proof system, and it is not a substitute for SMT solvers or proof assistants — it is a bridge into them.