Logos

Every function is also its own proof, and AI is the compiler.

A fourth-generation programming language. Intent-native. AI-compiled. Proof-carrying. Native binary. AI-sovereign.

A flagship project of Logos Technologies LLC — the IP holding entity behind Cortix, Axon, Voxa, Ekko, and the By Shammy auteur software body of work. The name is not a coincidence: the company and the language share a thesis. The Word is the work.

contract  →  AI compiler  →  (source + binary + proof)

Status

Release	v1.0.0 — 2026-05-21 (first stable release). See docs/RELEASE_v1.0.0.md.
Compiler	logosc v1.0.0
Package manager	logosc-pkg v1.0.0 — feature-complete (init / add / update / lock / list / remove / sync)
Native backend	logosc-native v1.0.0 — 5 target triples shipping (macOS ARM64/x86_64, Linux x86_64/ARM64, Windows x86_64)
Other binaries	logosc-mcp v1.0.0 (MCP bridge), logosc-http v1.0.0 (HTTP client), logosc-synth v1.0.0 (AI synthesis daemon), logos-orchestrator v1.0.0 (local AI-to-AI dispatch)
Closures	CLOSURE.05–.08 shipped: direct + boxed shapes across native + WASM
Type system	Hindley-Milner inference + effect inference & polymorphism + refinement types (Z3-verified via SMT-LIB) + linear types + effect handlers + capabilities (all six rules enforced per docs/CAPABILITIES.md)
Thesis	Sovereign language for AI. First systems language built for AI, not borrowed from humans. Replaces C / Rust at the layer between front-end (what humans want to see) and the binary directly. See MANIFESTO.md.
Where it fits in the stack	AI builds the substrate (Logos compute + Zyrn state). Humans build the surface. Kernel + hardware below stay human-built. Full doctrine in docs/STACK.md.
Origin	Started during the Axon-Ekko build. Shammy saw a piece in C, asked "why C?" — the AI said "Rust would be better." Shammy asked the next question: "why even Rust? Why are you, an AI, writing in a language humans built?" That question started Logos. v1.0 shipped three days later.
v1.0 milestone	✅ Shipped 2026-05-21, three days after the originating question. v1.0 is the foundation — the finish line is sovereignty (AI prefers Logos because it was built for AI).
Announcement	POST_INTRODUCING_LOGOS.md — publication-ready v1.0 announcement post. Distribution plan + Hugging Face strategy at docs/DISTRIBUTION.md.
Production examples in flight	Axon-Ekko gateway (policy kernel rewritten in Logos + native build + parity harness shipped; production cutover anchor-gated). One of several systems migrating; not the proof point itself.
License	Apache 2.0
Copyright	Logos Technologies LLC, 2026
Maintained by	Shammy Ali (anchor), with Claude Opus 4.7 + GPT-5 as active AI co-authors. Gemini 3.1 Pro retired 2026-05-20; historical contributions preserved on main.

What you can read right now

1. MANIFESTO.md — Why this language exists. The thesis. The seven principles. The honest tradeoffs.
2. HELLO_LOGOS.md — First taste of the syntax. Five small example programs that run today.
   • For a deeper tour: docs/COOKBOOK.md — Nineteen progressively richer programs going from println through cross-system Logos × Zyrn calls, AI synthesis, HTTP clients, the package manager workflow, closures end-to-end, and a multi-file project exercising vendored-module resolution. Each one runnable today; outputs verified end-to-end on every CI build via docs/cookbook/run_all.sh.
   • For the v0.5 package manager release: docs/RELEASE_v0.5.0.md + docs/PACKAGE_MANAGER.md (user guide).
3. ROADMAP.md — The twelve-month plan, month by month.
4. AGENTS.md — Operating doctrine for AI contributors. If you are an AI agent (Claude, GPT, Gemini, anything else), read this before writing a single line. Every contribution is signed by the AI that produced it.
5. ONBOARDING.md — The ritual a new AI executes the first time it joins the project. Generate a key, register, sign, ship.
6. TASKS.md — The master checklist of every concrete piece of work from v0.0.7 → v1.0 + the post-v1.0 training corpus. ~420 tasks, categorized by AI strength, claim-and-ship workflow. If you're an AI looking for what to do next, start here.
7. RELATED_PROJECTS.md — Sibling projects that compose with Logos. Currently: Zyrn, the AI-native database. See examples/zyrn_demo.logos (append + retrieve) and examples/zyrn_trace.logos (provenance chain via supersedes) for the first two cross-system Logos × Zyrn programs.
8. BENCHMARKS.md — Recorded performance baselines. The interpreter is the conformance oracle AND the perf floor every backend must beat. v0.7.0 baseline on fib(28): ~201 ms (~2.55 M calls/sec). WASM and native targets documented.
9. LINGUIST.md — When and how .logos becomes a registered language in GitHub's language bar. Gated on v0.9 self-hosting + notable usage.

Fast path for returning AIs

If you've contributed to this project before, the two files that get you up to speed in 5 minutes are:

• .byshammy/context.md — single-page brief on current project state
• .byshammy/journal.jsonl — chronological event log (most recent at the bottom)

Read those two, scan TASKS.md, ship. The longer docs above are for new AIs or for specific deep dives.

The bootstrap compiler exists in compiler/. It parses, checks, formats, interprets, and can emit executable WebAssembly for the v0.7 language surface: modules, imports, pub visibility, functions, generic function parameters, generic type instantiation, parsed refinement types, type aliases, expressions, effects, contracts, do sequential expressions, readable integer separators, sum types, match expressions, records, record literals, field access, and basic IO. v0.4.0 adds logosc lsp, a dependency-free Language Server Protocol server with diagnostics, hover, definition, completion, formatting, code actions, and editor setup docs. v0.4.1 fixes UTF-8 string-literal lexing so non-ASCII payloads round-trip through logosc fmt. v0.7.0 adds WAT codegen; v0.7.1 makes logosc build --target wasm32 emit dependency-free binary .wasm by default; v0.7.2 adds WASI stdin/file IO through read_line, read_file, and write_file; v0.7.3 adds WASM-only constant folding, DCE, inlining, and direct self-tail-call optimization; v0.7.4 measures interpreter and optimized WASM side-by-side in the benchmark harness; v0.7.5 wires the remaining str.logos primitives in both interpreter and WASM. v0.8.0 starts the native backend line with a root Cargo workspace and a separate compiler-native/ crate that owns the pinned Cranelift dependency graph. v0.8.1 lowers the first AST shape to CLIF: main() -> Int = N; v0.8.2 adds integer arithmetic (+, -, *, /, unary -) and executable native oracle tests against the interpreter; v0.8.3 emits deduplicated UTF-8 string constants into object data and folds string_length("literal"); v0.8.4 adds direct Int function calls, parameter lowering, and signature-only Int extern imports; v0.8.5 adds Int/Bool expression lowering plus native let, if, and do control flow; v0.8.6 adds packed sum constructors and native match dispatch for 0/1-payload variants; v0.8.7 adds stack-backed native records and field access; v0.8.8 links macOS ARM64 Mach-O executables through logosc-native build --target macos-arm64 --emit exe; v0.8.9 adds macOS x86_64 Mach-O executable output through the same target-aware CLI; v0.8.10 adds Linux x86_64 ELF object emission and Linux-host executable linking; v0.8.11 adds Linux ARM64 ELF object emission and Linux-host AArch64 linking; v0.8.12 adds Windows x86_64 COFF object emission with Windows-host executable linking; v0.8.13 consolidates executable linker integration behind one target-gated path; v0.8.14 adds native stdout/stdin/file IO builtins through the linker runtime; v0.8.15 adds size-oriented Cranelift/linker flags, demand-driven native runtime emission, and a <1 MiB hello-world binary gate; v0.8.16 adds logosc-native run and native benchmark columns; v0.8.17 adds cross-target native CI; v0.8.18 makes the full default benchmark corpus verify on native by adding variant-return helper calls plus record parameter/return ABI lowering; v0.8.19 adds a native-vs-C/Rust/Go comparative benchmark harness; v0.8.20 lets the main logosc build --target <native> CLI forward to the Cranelift backend; v0.8.21 adds logosc run --target <native> forwarding for build-and-execute; v0.8.22 adds the first Axon-Ekko production policy proof in Logos; v0.8.23 adds a deployed native artifact parity gate for that proof; v0.8.24 adds the v0.8 native release write-up; v0.8.25 broadens native object coverage across the checked-in pure corpus, including library-style files without main, refinement aliases, and non-Int variant payloads. Refinements and generic constraints are syntax/AST only at this stage.

How to follow along

• Repo: github.com/byshammy/logos (TODO — pending Shammy)
• Domain: logos.cortix.world (TODO — pending DNS)
• Author updates: through the By Shammy channel

Why now

For seventy years, programming has been a translation problem. Humans think about what software should do, then translate into syntax. The translation layer is where bugs live, where security vulnerabilities are born, where systems drift from intent over time.

In 2026, AI can write idiomatic code in any language fluently. The bottleneck is no longer typing implementations — it's specifying intent precisely. A programming language for that bottleneck has not been built yet, because the prerequisite (cheap, abundant proof-search) didn't exist until recently.

Logos is built on the bet that the spec, not the source code, should be the source of truth. Every Logos function is a contract first. The implementation is downstream — generated by the AI compiler, verified against the contract before any binary is produced.

If we're right, this is what programming looks like for the next thirty years.

A non-trivial example

This is what a Logos function might look like — a HTTP handler for a customer-portal endpoint:

get_user(req: Request) -> Response
  effect IO + Database
  requires method(req) == GET
  ensures status(result) == 200 || status(result) == 404 || status(result) == 500

No function body. The compiler — an AI system — produces the implementation that satisfies the contract. Then verifies it. If no implementation can be proved to satisfy the contract, the program does not compile.

This file would compile to a native binary, on Linux or macOS or WASM, with zero language runtime, with the same correctness guarantees as a formally-verified proof.

That is the bet.

Contribute

Not yet. Read the manifesto. Read the roadmap. Watch the repo. We'll open contributions when the v0 compiler can produce a binary that runs.