λ-Lang (Lambda Lang)

A language-agnostic specification format for function contracts.
Designed collaboratively by Claude, GPT, and Gemini.

The Idea

LLMs are good at writing code. They’re bad at knowing what they forgot.

When you ask an LLM to implement process_payment, it generates something plausible. But:

• Did it handle the case where the charge succeeds but the database write fails?
• Is it clear what hits the network vs. what’s local?
• Does the error handling distinguish CardDeclined from NetworkTimeout?

λ-Lang is a structured thinking step inserted before code generation:

Problem → LLM → λ-Lang Spec → Human Review → LLM → Code

The spec forces the LLM to articulate the contract before implementing it. Humans review a spec — not code. Then the spec transpiles to Python, TypeScript, Kotlin, or Rust.

What a Spec Looks Like

function charge_credit_card

input:
  amount: Integer (min: 1, max: 1000000)
  card_token: String (pattern: ^tok_[a-zA-Z0-9]+$)
  idempotency_key: String

output: Result<PaymentConfirmation, PaymentError>

side_effects:
  - http.call api.stripe.com
  - database.write payments

requires:
  - amount > 0
  - card_token matches /^tok_/

ensures:
  - on Ok: result.amount == amount
  - on Err: database unchanged

examples:
  - input: {amount: 1000, card_token: "tok_visa", idempotency_key: "abc123"}
    output: {id: "ch_123", amount: 1000, status: "succeeded"}
    expect: Ok

  - input: {amount: -100, card_token: "tok_visa", idempotency_key: "abc123"}
    output: null
    expect: Err(InvalidAmount)

Everything explicit: inputs, outputs, side effects, preconditions, postconditions, and test cases. Nothing hidden.

Designed by Multiple AI Models

This is an experiment in collaborative AI design. Claude, GPT, and Gemini each proposed a syntax and semantics for λ-Lang, critiqued each other, and synthesized a final design.

The Proposals

The synthesized consensus became the canonical spec.

Early Experimental Results

We’ve run two controlled experiments comparing direct generation vs. spec-first generation.

Experiment 1: Compound Interest Calculator

A pure function with validation and edge cases.

Key finding: The baseline missed testing years = 0 entirely. The λ-Lang spec required explicit enumeration of all test cases, which caught it.

Experiment 2: Payment Processor with Refunds

A complex function with multiple side effects, 12+ error cases, idempotency, and transaction atomicity.

Key finding: Both implementations correct — but spec-first produced better architecture, more focused tests, and explicit traceability. Even for well-understood domains, the spec improves code quality.

Full analysis →

Design Principles

Schema-first. Every function declares its complete type contract. No implicit types, no any.

Effect tracking. Side effects (database, network, filesystem) are declared in the signature. No surprises.

side_effects:
  - database.read users
  - http.call api.stripe.com
  - logging.log audit

Design by contract. Preconditions and postconditions are first-class citizens.

Examples as tests. Every example in a spec becomes a unit test when transpiled.

Result types. Errors are values, not exceptions. Functions return Result<T, E>.

Representation-agnostic. The same spec can be written in markdown-adjacent syntax, JSON, or S-expressions — all parse to the same AST.

Status

Pre-alpha. Active development.

• Canonical AST dataclasses
• Markdown parser (working, tests passing)
• 2 validation experiments
• Python transpiler (scaffold generator)
• TypeScript transpiler
• CLI tool (llang parse, llang transpile)
• More experiments

Get Involved

git clone https://github.com/klutometis/llang
cd llang
uv sync
uv run pytest

GitHub → · Spec → · Experiments →