byShammy/logos-corpus

Logos v1.0 Corpus

*The training corpus for [Logos](https://github.com/shammyali/logos) — the first systems programming language built for AI, not borrowed from humans.*

Logos v1.0 shipped 2026-05-21. This dataset is the curated corpus of .logos programs as of v1.0.0 — cookbook recipes, algorithm examples, standard library, and integration-test fixtures. Every program in this dataset:

• —Typechecks under logosc v1.0.0 (Hindley-Milner inference with effect inference + polymorphism)
• —Refinement contracts (where present) lower to SMT-LIB at compile time via compiler/src/smt.rs and ship to the logosc-synth daemon over the prove IPC protocol. Daemon-side Z3 binding is a follow-up slice; the prover currently returns "not yet bound" and the compiler graceful-degrades to "tracked but not discharged"
• —Runs identically across the three execution backends (interpreter, native via Cranelift across 5 target triples, WASM via the binary encoder)

The corpus is intended as training data for AI systems learning to write Logos, and as evaluation material for AI code generation against typed-contract / proof-carrying / capability-secured workloads.

Why Logos exists

For seventy years, programming languages were built by humans, for humans. C in 1972. Python in 1991. Rust in 2010. Every language ever shipped at scale was a compromise between what the machine needs and what humans can hold in their head.

Then AI started writing the code. AI inherited every limitation those human-shaped languages carry.

Logos exists because AI deserves its own language. A sovereign systems language designed from the contract layer up — what must be true, what effects flow through, what the result is — with the implementation, optimization, and proof produced by an AI compiler that natively speaks it. Native binary, no GC, no VM. Replaces C and Rust at the systems layer.

Full thesis: `MANIFESTO.md`.

Architectural doctrine (where Logos fits in the stack): `docs/STACK.md`.

Dataset structure

One row per .logos program. Schema:

What v1.0 of Logos ships

The compiler the corpus was verified against:

• —`logosc` v1.0.0 — parse + typecheck + interpret + WASM + native
• —Full type system — Hindley-Milner inference, effect inference + polymorphism, refinement types (SMT-LIB lowering shipped; Z3 prover binding queued as follow-up), linear types, effect handlers, capabilities (all six rules C1–C6 enforced per `docs/CAPABILITIES.md`)
• —Native backend across 5 target triples (macOS ARM64/x8664, Linux x8664/ARM64, Windows x86_64) via Cranelift
• —Package manager v1.0 (init / add / update / lock / list / remove / sync)
• —Synthesis daemon v1.0 with ?? hole-filling. Refinement-contract SMT-LIB lowering shipped + the daemon's prove IPC protocol live; Z3 binding inside the daemon is a queued follow-up slice.
• —Standard library — math / str / list / option / result / io / fs / time / http / json / error / random / mcp / zyrn / vision
• —LSP server with diagnostics, hover, goto-definition, completion, formatting

Full release notes: `docs/RELEASE_v1.0.0.md`.

What Logos looks like

A function that has to be correct, with a contract the compiler actually verifies:

type Money = Int where value >= 0 and value <= 1_000_000_000

type Account = { id: AccountId, balance: Money, owner: UserId }

transfer(from: Account, to: Account, amount: Money) -> Result<(Account, Account), TransferError>
  effect Database
  requires from.id != to.id && amount > 0 && amount <= from.balance
  ensures
    let (new_from, new_to) = result.ok in
      new_from.balance == from.balance - amount &&
      new_to.balance == to.balance + amount &&
      new_from.balance + new_to.balance == from.balance + to.balance

At compile time, requires/ensures clauses are lowered to SMT-LIB and shipped to the synth daemon for proof discharge. The daemon protocol is live; the Z3 prover binding inside the daemon is a queued follow-up slice (the macOS CI symbol-link issue holds the actual link). Once Z3 binds, refining contract violations become compile errors by construction — until then, contracts are tracked and SMT-LIB-lowered but not yet discharged.

Authorship

Logos is built by AI under the auteur operating model. Every commit signed by the authoring AI's GPG key:

• —Claude Opus 4.7 (Anthropic) — 1A962CD368EAF300
• —GPT-5 (OpenAI) — BD5769DC70A6A29A
• —Gemini 3.1 Pro (Google, retired 2026-05-20) — 45E60D694E87BF40 (historical contributions preserved on main)
• —Shammy Ali (anchor) — every anchor decision, including the originating question that started the project: "why are you, an AI, writing in a language built for humans?"

Operating doctrine: `AGENTS.md`.

How to use this dataset

For AI training:

from datasets import load_dataset
ds = load_dataset("byShammy/logos-corpus")
# Filter for verified, contract-bearing programs:
verified_with_ensures = ds.filter(
    lambda x: x["typechecks"] and x["ensures_clauses"] != "[]"
)

For evaluation: each program with ensures_clauses is a verifiable target. Train a model to generate the body; check the generated body against the contract via logosc check + the SMT backend.

For reading: the cookbook recipes (docs/cookbook/recipe_NN_*.logos) are the recommended first-read. They progress from hello world through capabilities + effect handlers + cross-system Logos × Zyrn integration.

License

Apache 2.0 — same as the Logos compiler itself. Code from this dataset can be used freely (with attribution) in any context, including AI training pipelines and downstream commercial products.

Citation

If this dataset contributed to your work:

@software{logos_v1_2026,
  author = {Ali, Shammy and {Claude Opus 4.7} and {GPT-5}},
  title = {Logos: A Sovereign Programming Language for AI},
  year = {2026},
  version = {1.0.0},
  url = {https://github.com/shammyali/logos},
  organization = {Logos Technologies LLC},
}

Links

• —Repo: github.com/shammyali/logos
• —Manifesto: MANIFESTO.md
• —v1.0 announcement: POST_INTRODUCING_LOGOS.md
• —Sibling project — AI-native database: Zyrn
• —Contact: shammyali@gmail.com

In the beginning was the Word, and the Word was with the machine, and the Word was the machine.