Zerdali

Türkçe · English · Deutsch · Français · Español · 中文 · العربية · AI/LLM

A language whose signatures carry what a function does and what data it touches — effects and information-flow labels, checked by the compiler. Two independent implementations that must agree byte for byte, and a compiler written in its own language that reproduces itself exactly.

effect io { print(msg: Str@public) -> Unit }

fn greet(name: Str@personal) -> Str@personal { "Dear " + name }

// Only the answer to "is there a record?" leaves. The name itself does not.
fn exists(name: Str@personal) -> Bool@public {
  declassify(str_len(greet(name)) > 6, public,
    "existence only; no field of the record travels")
}

fn main() -> Unit !{io.print} {
  io.print("registered: " + show(exists("Ayse")))
}

Two things in those signatures that most languages cannot say:

• !{io.print} — the complete list of effects this function may perform. Perform one you did not declare and it does not compile.
• @personal → @public — where the data may go, and the single point where that may narrow: declassify, which requires a written reason. zerdali audit collects every one of them.

---

Why another language

Two ideas have been well understood in research for twenty years, and each exists somewhere in practice — but never in the same signature.

What a function does. Algebraic effects: Koka, Eff, Frank, Unison. OCaml 5 has the runtime mechanism but keeps it out of the types. Haskell has IO, but a single IO covers reading a file, launching a process, and printing a line — it says something happens, not what.

What data a function touches. Information-flow types: Jif, FlowCaml, Paragon. Academic, mostly dormant, and none of them has an effect system.

So today you can know that a function touches the disk, or you can know that a value is personal data — but you cannot get both from one signature, in one checked language, with one compiler.

That gap is the reason this language exists. The two questions are the same question: what may this code reach, and what may reach out of it? Answering only one of them leaves the other to code review.

	effects in the type	information flow in the type	termination checked	single static binary
Go, Java, Python, JS	—	—	—	Go only
Rust	—	—	—	yes
Haskell	coarse (IO covers all)	—	—	—
OCaml 5	runtime only, not in types	—	—	—
Koka, Eff, Frank	yes	—	Koka: yes	—
Unison	yes (abilities)	—	—	—
Jif, FlowCaml	—	yes	—	—
Idris, Agda	—	—	yes	—
Zerdali	yes	yes	yes	yes

Zerdali did not invent either column. The effect row is Koka's idea, div.loop included; labels and declassify come from the Jif/FlowCaml line. What is new is the row where both columns are filled at once — and what that combination makes possible downstream: hermetic tests with no mocking framework, and a capability report you can read before the program runs.

What is here that is not elsewhere

1. Effect row and label in one signature. fn f(x: Str@personal) -> Bool@public !{fs.read} says, in one line, what f may do and where its data may go. No other language checks both.
2. declassify demands a written reason. Narrowing a label is not a cast — it is a decision, and the compiler makes you record why. Those reasons are not comments: audit collects them into the program's declassification report.
3. audit — the capability report, before running. Every function's effects, every label reach, every declassification with its reason. What a program may do, read without running it.
4. test runs with nothing granted. A test that reaches for the real disk fails. A test that needs a file handles fs.read and provides one, in the language, checked by the compiler. There is no mocking framework because none is needed.
5. Termination is proved or declared. There are no loops; recursion carries every iteration. Any function in a call cycle must declare !{div.loop} unless the recursion is structurally decreasing. So pure here means "no side effects and terminates".
6. Ownership is declared, not inferred. own Buf makes a write in place instead of a copy. It is written in the signature, never guessed — inference would have to give the same answer in both implementations, which would make it part of the language definition, and the definition would stop being readable.
7. Two implementations, held to byte-for-byte agreement. A Python reference and a self-hosted compiler, run against each other on every change. And the compiler reproduces itself exactly: compiling its own source with the binary it produced yields the identical binary. Checked, not assumed.
8. A language card built for machines, and measured. LLM.md is ~2.7k tokens and is the whole language. Thirteen models from three vendors were measured writing Zerdali from that card alone — the numbers are below, and the harness is in the repository.

---

The language in ten examples

Every example below is a file in examples/. The outputs are not typed by hand — test_examples.py runs each one and compares against the line in its comment, so nothing here can go stale in silence.

1 — An effect is declared, then performed

effect io { print(msg: Str@public) -> Unit }

fn main() -> Unit !{io.print} {
  io.print("merhaba, Zerdali")
}

$ zerdali run 01-hello.zd
merhaba, Zerdali

io.print is not a magic function. It is an operation of a declared effect, and every function that performs it says so.

2 — The effect row is contagious; the pure stays pure

fn polite(name: Str) -> Str { "Sayin " + name }              // no row: performs nothing

fn shout(msg: Str) -> Unit !{io.print} { io.print(msg) }

fn greet(name: Str) -> Unit !{io.print} {                    // must declare it too
  shout("SELAM, " + name);
  shout(polite(name))
}

Delete the row from either one and the compiler answers ZD302 — and tells you which line to write.

3 — A handler replaces the mocking framework

effect fs { read(path: Str@public) -> Str@public }

fn read_port() -> Str !{fs.read} { fs.read("/etc/app.conf") }

fn checked() -> Str {                       // note: no effect row
  handle read_port() with { fs.read(p) => "8080" }
}

$ zerdali run 03-handlers.zd
8080

The handler answers the operation, and the effect leaves the signature — checked no longer declares fs.read, because it no longer does it. That is not a testing library. It is the language.

4 — A label says where data may go

fn greet(name: Str@personal) -> Str@personal { "Sayin " + name }

fn exists(name: Str@personal) -> Bool@public {
  declassify(
    str_len(greet(name)) > 6,
    public,
    "varlik bilgisi; kaydin hicbir alani tasinmiyor"
  )
}

$ zerdali audit 04-labels.zd | tail -1
  personal -> public at <root>:22: varlik bilgisi; kaydin hicbir alani tasinmiyor

Everything derived from name stays personal — including a comparison, because which branch was taken is information too. Passing it to something that returns public is ZD301. The only way to narrow is declassify, and it costs you a sentence.

5 — Data types and the match that consumes them

data Shape { Circle(r: Int) | Square(a: Int) | Dot }

fn area(s: Shape) -> Int !{exn.raise} {
  match s {
    Circle(r) => r * r * 314 / 100,
    Square(a) => a * a,
    Dot => 0
  }
}

$ zerdali run 05-data-match.zd
314

A match that misses a constructor does not compile. There is no default arm to hide behind.

6 — Recursion, and the proof that it ends

data Nums { Nil | Cons(head: Int, tail: Nums) }

// Proved: `rest` is bound by the `match` on `l`. No row needed.
fn total(l: Nums) -> Int {
  match l { Nil => 0, Cons(v, rest) => v + total(rest) }
}

// Arithmetic is not proved, so `div.loop` stays in the signature.
fn fact(n: Int) -> Int !{div.loop} {
  if n <= 1 { 1 } else { n * fact(n - 1) }
}

The proof is deliberately simple: an argument shrinks when it is a variable bound by a match on the corresponding parameter. n - 1 shrinks to a human eye, and the checker does not look for it. That is a decision, not an omission — the proof staying readable is worth more than the proved set being larger.

7 — Modules

// geom.zd
pub fn scaled(x: Int, k: Int) -> Int { x * k }
pub fn area(w: Int, h: Int) -> Int { scaled(w, h) }

// 07-modules.zd
use geom

fn main() -> Unit !{io.print} {
  io.print("alan: " + show(geom.area(4, 6)))
}

$ zerdali run 07-modules.zd
alan: 24

pub marks what leaves a module; calls are qualified. scaled is public here only to show that it can be — a module's private functions stay private.

8 — Buf and own: unboxed numbers, writes without copies

fn ramp(b: own Buf Float, i: Int) -> own Buf Float !{exn.raise, div.loop} {
  if i >= buf_len(b) { b } else { ramp(buf_set(b, i, to_float(i + 1)), i + 1) }
}

fn main() -> Unit !{io.print, exn.raise, div.loop} {
  let v: Buf Float = ramp(buf_floats(5), 0);
  io.print("nokta carpim: " + show(to_int(buf_dot(v, v))))    // 55
}

buf_set returns a value — whoever held the old buffer still sees the old one. That rule does not move; what moves is the cost. When the signature says own, nobody else holds it, and the write happens in place. buf_dot is a vectorised runtime kernel: two doubles at a time.

9 — Tests, with nothing granted

fn config_port() -> Str !{fs.read} { fs.read("/etc/app.conf") }

fn test_pure_arithmetic() -> Bool { 2 + 2 == 4 }

// A function that reads a file, tested without a file.
fn test_config_is_read() -> Bool {
  handle config_port() with { fs.read(p) => "8080" } == "8080"
}

$ zerdali test 09-tests.zd
3/3 hermetic tests pass

A failing test only says returned false. The standard library's assert closes that:

use assert

fn test_adds() -> Bool !{exn.raise} { assert.eq_int(add(2, 2), 5) }

fn test_greets() -> Bool !{exn.raise} { assert.eq_str_at("greeting", "hi", "hello") }

$ zdc test demo.zd
FAIL  test_adds  uncaught error: expected 5, got 4
FAIL  test_greets  uncaught error: greeting: expected "hello", got "hi"

An assertion failure is a raise, and the runner already carries the raised message — so assert needed no change to either implementation. It also asserts the other direction: assert.raises(f) and assert.raises_with(f, "index 9") require that something does fail, and for the right reason.

A test's signature may carry only exn.raise and div.loop. Anything else would tie the answer to something unwritten — and then the test would stop being a measurement.

10 — A real program: file, arguments, --allow

$ zerdali run --allow fs.read,sys.argc,sys.arg 10-wordcount.zd -- 01-hello.zd
01-hello.zd: 14 satir

Capabilities are granted at the command line. A program whose signature asks for fs.read and is not granted it stops with a message naming the effect — the signature is the good error, the empty capability set is the one that cannot be talked out of.

Read them in order in examples/: the first three are what the language does, 04 is why it exists, the rest is daily work.

---

For LLMs and agents

One of the three design goals was that a model should be able to pick this language up from a short document and get it right. That is a claim you can only make by measuring it, so the language ships with both halves:

• LLM.md — the language card. About 2.7k tokens, and it is the whole language: every form, every rule, every deliberate limit. This is the file handed to the models in the benchmark below — byte-identical on every request.
• docs/i18n/documentation.ai.md — the dense machine-first reference: every command, every flag, an honest status block.
• The compiler's diagnostics are the feedback channel. Every error carries the rule it broke (rule: effects-declared-in-signature) and, where it can, the line to write. zdc explain ZD302 prints the rule in full. In the benchmark the model gets nothing back but the diagnostic — no hints, no solution.
• zdc lsp and zdc serve expose checking, diagnostics and repairs over LSP and JSON, for agents that would rather ask than parse.

If you are an agent reading this repository: start at LLM.md. It is enough.

How well models write it

Measured 2026-08-30 with eval_model.py. Each model gets the card, a task brief, and a submit tool; the submitted program is compiled and run; if it is not green, the only thing returned is the compiler's own diagnostic. So the number is how many rounds of talking to the compiler it took to get to correct. Four tasks × 5 runs = 20 runs per model, same card for all thirteen.

vendor	model	green	first try	median rounds	min–max
Anthropic	claude-opus-4-8	20/20	20/20	1	1–1
Anthropic	claude-fable-5	20/20	20/20	1	1–1
Anthropic	claude-opus-5	20/20	19/20	1	1–2
Anthropic	claude-sonnet-4-6	20/20	19/20	1	1–2
Google	gemini-3.1-pro-preview	20/20	18/20	1	1–2
Google	gemini-3-flash-preview	20/20	18/20	1	1–2
Anthropic	claude-opus-4-7	20/20	18/20	1	1–3
OpenAI	gpt-5.1	20/20	17/20	1	1–4
Anthropic	claude-sonnet-5	20/20	15/20	1	1–3
OpenAI	gpt-5-mini	20/20	11/20	1	1–4
Anthropic	claude-haiku-4-5	18/20	4/20	3	1–6
Google	gemini-3.1-flash-lite	17/20	6/20	2	1–6
OpenAI	gpt-5-nano	7/20	1/20	2	1–3

Ten of thirteen models reach green in all twenty runs. The separation is not whether — it is in how many rounds, and first-try rates run from 20/20 down to 1/20.

The finding that matters for the language. Counting which rule the failed submissions broke:

count	rule
46	no-implicit-declassification
13	variables-must-be-bound
13	effects-declared-in-signature
12	unique-function-name
8	match-needs-a-data-type

Information flow is the one genuinely new thing to learn. The effect row is not hard for models — the compiler names the line to write, and the model writes it. The label is different: declassify asks for a decision, and the compiler cannot write your justification for you.

What makes the three vendors comparable is eval_vendors.py: the protocol does not change. run_task is literally the same code for all three; the adapters only translate the request. Had there been three loops, no one could say whether a difference came from the model or from the loop. Reasoning effort was equalised at high across all three (three different parameter names). Full method and per-task breakdown: docs/model-benchmark.md.

---

Quick start

$ python3 zerdali.py check policy.zd
$ python3 zerdali.py run   sample.zd
$ python3 zerdali.py audit policy.zd
$ python3 zerdali.py test  tests.zd
$ python3 zerdali.py build sample.zd -o sample

The reference implementation is one Python file with no dependencies. To build the self-hosted compiler and use it instead:

$ ZERDALI_HEAP_MB=6000 python3 zerdali.py build zdc.zd -o zdc
$ ./zdc check policy.zd
0 error(s), 1 note(s)

zdc is a static binary with no runtime. Both implementations answer all sixteen commands — check, run, build, test, audit, doc, fmt, fix, holes, debug, explain, spec, search, serve, lsp, pkg — and are held to giving the same answer.

Library modules resolve from the entry file's directory, then from vendor/. zdc pkg sync fills vendor/ and zdc pkg verify checks it against the lock, so a build can be reproduced.

Documentation

• Full documentation: Türkçe · English · Deutsch · Français · Español · 中文 · العربية
• Language card for models: LLM.md — start here if you are an LLM or an agent.
• Machine-first reference: documentation.ai.md
• examples/ · GUIDE.md — the tutorial · SPEC.md — the normative rules · V1.md — what v1 means and where the edges are
• docs/model-benchmark.md — the measurement above, in full

Download

Ready to download from the v1.0.0 release. Nothing was packaged until six suites passed, test_fixpoint among them.

zerdali_1.0.0_amd64.deb	Debian / Ubuntu — zdc + reference + docs
zerdali-1.0.0-linux-x86_64.tar.gz	Linux x86-64
zerdali-1.0.0-any-python.zip	reference implementation only, any platform

About

Zerdali is open source under the MIT licence.

It is a young project, and the honest status is this: it is tested against itself thoroughly — two implementations, a differential suite, a self-reproduction fixpoint — and by nobody else. There has been no independent review and there are no users beyond its own development. The lesson that keeps coming back is that the differential says the two implementations agree, not that they are right: every bug worth finding was invisible because no program in the corpus exercised it.

Issues and patches are welcome.

MIT · LICENSE