# agentlanguages.dev > A community-edited catalogue of programming languages designed for AI agents to author code. 28 projects organised around three philosophical camps — syntactic, verification, orchestration — plus adjacent and unclassified buckets. As of 20 May 2026. 28 languages tracked. Originally catalogued in a post ["Three camps alike in dignity"](https://negroniventurestudios.com/2026/05/20/three-camps-alike-in-dignity/) written for the Negroni Venture Studios blog. ## The taxonomy Three camps disagree on how to frame the problem. The **Syntactic** camp says the problem is representational — strip ambiguity at the token level. The **Verification** camp says it's semantic — make contracts mechanically checkable. The **Orchestration** camp says it isn't a language problem at all — constrain how agents coordinate. The catalogue below treats them as evidence that this disagreement is real. ## Syntactic > If the problem is that models trip on syntax, the fix is to strip ambiguity from the syntax itself. The syntactic camp treats the problem as one of representation. Models choke on tokens that mean different things in different positions, on operators that need disambiguation, on whitespace that might or might not be load-bearing. Their answer: build a syntax where every token has one job. The strongest entries replace text with structure (X07's JSON ASTs), eliminate operators in favour of keywords (NERD), or surface intermediate representations as the user-facing form (Magpie's SSA). The weakest are exercises in extreme density — one-character opcodes — that read more as conceptual art than as production languages. What unites them is a belief that the LLM's job is easier if the surface is simpler. What divides them from the verification camp is the absence of any mechanism for the compiler to catch what the model gets wrong. ## Verification > The model doesn't need to be right. It needs to be checkable. The verification camp accepts that LLMs will keep making semantic errors and asks a different question: can the compiler catch them? Their answer is mandatory contracts, refinement types, effect systems, and SMT-backed proofs — the machinery of formal methods, repurposed as a guardrail for generative code. This is the camp with the most established theoretical foundation (the work goes back to ML, Coq, Dafny, and Lean) and also the most mature implementations. MoonBit ships a full toolchain with ICSE-published research; Vera ships measured benchmark wins against Python on zero training data; AILANG claims to be written autonomously by its own coordinator. The provocative entry is Prove — same diagnosis, opposite conclusion. It uses verification to make the language *resistant* to AI generation. The licence explicitly prohibits training use. Same camp, opposite politics. ## Orchestration > It isn't a language problem. It's an agent-coordination problem. The orchestration camp re-frames the question. The trouble with LLM-authored code, they argue, isn't any specific defect in the code — it's that agents need to be sequenced, sandboxed, audited, and approved by humans at the right points. The language is just the substrate; the runtime is where the action is. Some entries here are academic (Pel from CMU, Quasar from Penn); some are infrastructure (Marsha treats the LLM as the compiler itself); one is a serious engineering effort aimed squarely at regulated industries (Boruna's hash-chained evidence bundles and deterministic replay). This camp overlaps the most with the others — Boruna includes a type checker and capability system; Quasar adds conformal prediction. The line between “language for agents” and “framework for agents” is genuinely blurry here, which is itself informative. ## The full catalogue (as of 20 May 2026) Every language designed for LLMs or agents to author code. ### Syntactic camp - **[B-IR](https://agentlanguages.dev/languages/b-ir.md)** — A Jason Hall blog post on three attempts at an LLM-optimised language: B-IR with unicode opcodes, TBIR with control characters the model rewrote into English keywords, and Loom with pre/postconditions and stable error codes. - **[Codong](https://agentlanguages.dev/languages/codong.md)** — Designed for AI to write, with one canonical way to express every operation. Nine bundled modules, structured JSON errors with fix/retry fields, ? operator for propagation. Compiles to Go IR, then native via go build. - **[Laze](https://agentlanguages.dev/languages/laze.md)** — Minimal indentation-based syntax with no punctuation. A Python bootstrap compiler emits C in memory and pipes it to cc -O2. Framed by its author as a weekend experiment in what an LLM produces when asked to design a language for itself. - **[Magpie](https://agentlanguages.dev/languages/magpie.md)** — SSA as the surface syntax. Every value %-prefixed and typed at definition; one canonical way to express each operation; compiles to native via LLVM. - **[Mog](https://agentlanguages.dev/languages/mog.md)** — Statically typed embedded language with flat operators (no precedence) and host-granted capabilities. Full spec fits in 3,200 tokens. Compiles to native via a safe-Rust port of QBE. - **[NERD](https://agentlanguages.dev/languages/nerd.md)** — No Effort Required, Done. Replaces every operator with an English keyword on the bet that LLM tokenisers spend fewer tokens on words than on symbols. Built-in MCP client and LLM call primitives. - **[Sever](https://agentlanguages.dev/languages/sever.md)** — Single-character opcodes for extreme density. The author's README disclaims the entire repository as Claude-generated and explicitly frames the project as a thought experiment or art piece. - **[Tacit](https://agentlanguages.dev/languages/tacit.md)** — AST as the source of truth. Canonical byte-exact text, BLAKE3-addressed definitions, DeBruijn indices, typed Hole nodes for malformed code, and explicit effects in function signatures. - **[X07](https://agentlanguages.dev/languages/x07.md)** — Eliminates text syntax. Programs are canonical JSON ASTs (x07AST); edits are RFC 6902 JSON Patch operations; diagnostics ship as stable JSON with quickfixes the toolchain applies deterministically. ### Verification camp - **[AILANG](https://agentlanguages.dev/languages/ailang.md)** — Row-polymorphic Hindley-Milner with capability-based effects (IO, FS, Net, Clock, AI). No loops, lambda calculus only. Written autonomously by AI agents. - **[Aver](https://agentlanguages.dev/languages/aver.md)** — Every function carries intent, declared effects, and a colocated verify block. Pure verify blocks export to Lean 4 theorems and Dafny lemmas; effectful ones lift through the Oracle proof export. - **[Intent](https://agentlanguages.dev/languages/intent.md)** — Mandatory preconditions, postconditions, and entity invariants. Z3 SMT verification via intentc verify. Natural-language intent blocks that resolve to specific contract references. One source file compiles to Rust, JavaScript, and WebAssembly. - **[MoonBit](https://agentlanguages.dev/languages/moonbit.md)** — AI-friendly general-purpose language. ICSE 2024 paper on real-time semantics-aware token sampling. Three years of training data. - **[NanoLang](https://agentlanguages.dev/languages/nanolang.md)** — Mandatory shadow test blocks on every function. The proved core (NanoCore) has 193 Coq theorems with zero axioms. Multi-target codegen across C, WebAssembly, LLVM IR, PTX, and RISC-V. - **[Pact](https://agentlanguages.dev/languages/pact.md)** — Intent blocks on every function and route, pipeline syntax, explicit effects, errors as types. Single binary that ships an HTTP server, SQLite, an LSP, and an MCP server with five tools. - **[Prove](https://agentlanguages.dev/languages/prove.md)** — Intent-first language with verb-based IO, refinement types, and contracts. Source is covered by the Prove Source License v1.0, which prohibits use as AI training data. - **[Raskell](https://agentlanguages.dev/languages/raskell.md)** — Not a new language. The thesis is that declarative Haskell already plays to LLM strengths and the barrier is toolchain friction. hx wraps cabal/stack/ghcup/HLS in Rust; BHC is a clean-slate Haskell 2026 compiler with per-profile runtimes. - **[Vera](https://agentlanguages.dev/languages/vera.md)** — Mandatory contracts on every function. Z3 SMT verification. Typed slot references replace variable names. LLM inference is a first-class typed effect. - **[Zero](https://agentlanguages.dev/languages/zero.md)** — Vercel Labs' agent-first systems language. Sub-10 KiB native binaries. Structured JSON diagnostics with stable codes and typed repair plans. One obvious path. ### Orchestration camp - **[Boruna](https://agentlanguages.dev/languages/boruna.md)** — Deterministic, capability-safe workflow execution. Every effect declared, policy-gated. Hash-chained tamper-evident evidence bundles. - **[Lumen](https://agentlanguages.dev/languages/lumen.md)** — Markdown-native source (.lm.md). Algebraic effects, grants for tool and model calls, @deterministic compile-time enforcement, and pipeline / machine / memory process kinds. A language for humans authoring agent workflows. - **[Marsha](https://agentlanguages.dev/languages/marsha.md)** — Functional, English-based language whose .mrsh files (declaration, description, examples) are compiled to tested Python by an LLM. Alpha implementation; last maintainer activity early Aug 2023. - **[Pel](https://agentlanguages.dev/languages/pel.md)** — Lisp-flavoured language for orchestrating LLM agents, with capability control enforced at the grammar level and a REPeL self-healing loop modelled on Common Lisp restarts. - **[Quasar](https://agentlanguages.dev/languages/quasar.md)** — Penn group's LLM-agent language with automatic parallelisation, conformal-prediction reliability bounds, and approval-gated security; LLMs write a Python subset that transpiles to Quasar. ### Adjacent & unclassified Infrastructure that operates around these languages, or candidates that haven't shipped enough to classify. - **[Plumbing](https://agentlanguages.dev/languages/plumbing.md)** — A typed language for the wiring between agents. Symmetric monoidal category, typed channels, structural morphisms, agents as stateful morphisms with control ports. - **[Koru](https://agentlanguages.dev/languages/koru.md)** — Zig-superset systems language with event continuations, mandatory branch handling, phantom typing, and purity tracking. Pre-alpha — 'only ever been compiled on a single computer.' AI-First framing intentionally tongue-in-cheek. - **[Spec](https://agentlanguages.dev/languages/spec.md)** — v0.2 design proposal for a language-agnostic IR for agent-driven development. Six specialised agents (Product, Architect, Scrum, Developer, Tester, DevOps) collaborate on shared .spec.ir artefacts; language-specific code generation is downstream. - **[Valea](https://agentlanguages.dev/languages/valea.md)** — An AI-native systems programming language announced on Hacker News in March 2026. The Rust MVP compiler ships JSON diagnostics, a JSON AST exporter, a formatter, and a C backend. Public information beyond the repository README is limited. ## Methodology A community-edited catalogue of programming languages designed for AI agents to author code — not languages that *use* LLMs at runtime, but languages whose syntax, semantics, or runtime are deliberately shaped around an agent being the primary author. ### What counts The bar is intent. A language is in scope if its designers explicitly target LLMs or agents as authors — through token-friendly syntax, mechanically checkable contracts, agent-coordination primitives, or first-class effect declarations for model calls. A tool that calls an LLM at runtime (chatbots, autocomplete plug-ins, IDE assistants) is not in scope. A language whose only innovation is “works with Copilot” is not in scope. The line is the design intent, not the tooling. ### How to contribute Open a pull request adding a Markdown file to `src/content/languages/`. The [contribution guide](https://github.com/aallan/agentlanguages/blob/main/CONTRIBUTING.md) asks for evidence the project meets the inclusion bar and a self-classified camp with justification. The maintainer reviews each submission for fit, accuracy, and tone (the catalogue is descriptive, not promotional). Marginal cases get discussed in the PR thread. Edits to existing entries are welcome — especially corrections from the language's authors. ### For machines The catalogue is itself a machine-readable specification. Every detail page has a markdown companion at the same path with a `.md` extension, discoverable through `` and the [llmstxt.org](https://llmstxt.org) conventions. Use [/llms.txt](/llms.txt) for the short index, [/llms-full.txt](/llms-full.txt) for every entry in one file, or [/sitemap.xml](/sitemap.xml) for the full URL set. Agents and crawlers are explicitly welcome. --- HTML version: https://agentlanguages.dev/ Maintained by Alasdair Allan · [github.com/aallan/agentlanguages](https://github.com/aallan/agentlanguages)