QAL.
one round · every check · 0.28 s

An agent writes code and knows in the same round whether it is right.

In QAL, code does not live in files but as checked function nodes in a store. Every write is immediately typed, proven, tested and relinked with the whole program. The answer arrives in under half a second, as JSON.

Query&AgentLanguage
agent → qal_defineQAL
type Acct = { id: Int, balance: Int }

fn deposit(a: Acct, n: Int) -> Acct
  req n >= 1
  ens r.balance > a.balance
= Acct { id: a.id, balance: a.balance + n }

test deposit_adds =
  deposit(Acct { id: 1, balance: 5 }, 3).balance == 8
store → agent, same roundJSON
{
  "defined": ["Acct", "deposit", "deposit_adds": "added"],
  "proofs":  ["req n >= 1" at the call in deposit_adds: "proven",
             "ens r.balance > a.balance": "unknown", still checked at run time],
  "tests":   ["deposit_adds": passed],
  "warnings": [{ "code": "E0804", "kind": "property_traps",
    "message": "`deposit` trapped in 3 of 103 generated runs:
      Int overflow in `+` (64-bit) {left: 1, right: 9223372036854775807}",
    "hints": ["... say so with a `req` on `deposit` that bounds them"] }]
}

The real reply of qal_define to exactly this code, shortened, in 0.44 s. No test checked the overflow at a balance near the Int maximum; the property tests found it in the same round.

0.28 sone define with every check, 66 functions
0.43 sthe same at 1520 definitions
95 / 96stages with every hidden test green
11 / 13planted bugs E0807 reports without any test
The name

QAL stands for Query & Agent Language

Both halves of the name describe how the language works.

Q
Query

Code is queried, not searched

Code lives in a store instead of files. An agent queries it: who uses a function (qal_query), what a definition looks like (qal_view), how it changed (qal_history). Every answer is structured JSON, not text to be parsed first.

A
Agent

Built for whoever writes the code

The language is designed for AI agents, not for people at an editor. So every write checks everything at once, every error has a code, a path and a hint for the fix, and every effect on the outside world has to be granted explicitly.

Why now

The next step: languages for the time when agents write the code

Every widely used programming language was designed for people at an editor. Today AI agents write a growing share of code. QAL starts where that has moved the bottleneck.

What changed

Producing code has become cheap

An agent writes in seconds what takes a person hours. The amount of code grows faster than people can read and check it.

Where the bottleneck is now

Checking is expensive

In today's languages you find out later whether code is right: in a test run, a review, in production. An agent often does not find out at all, or too late.

What QAL makes of it

Checking is part of writing

Every write is typed, proven, tested and linked with the program at once. Trust comes from machine-checked guarantees, not from hope.

ConcernLanguages for peopleQAL, a language for agents
Where code livestext files you searchchecked nodes in a store you query
Error messagestext for peopleJSON with code, path and a hint for the fix
Testsa separate, later steprun with every write, as far as the change reaches
Contractscomments or runtime assertsproven by the Z3 prover when written
Side effectsinvisible in the codedeclared in the type and granted one by one
Silent regressionsfound by a person, with luckreported by the behaviour memory in the same round
AI calls in a programan unchecked API callan effect with a budget, recording and deterministic tests
Several agentsconflicts in version historyroles, leases, a merge gate and a signed history

Our thesis: the more code agents write, the less trust can come from a person reading every line. It has to come from the language itself. QAL is built around that idea. What of it is measured today, and what is not better yet, is below under numbers and limits.

One round

Five checks, one call

Other languages spread these steps over compiler, test run, linter and review. In QAL they are the answer to every write. The agent does not have to trigger any of them; a separate qal_test or qal_prove afterwards is not needed.

Types and effects

Does it fit?

Type checking, exhaustiveness of every match, and every function states what it may do: !io, !fs, !net, !db, !model.

Z3 proof

Does the contract hold?

Every ens, and every function's req at each call. A refuted contract is not stored; the diagnostic carries a counterexample.

Tests

Does anything break?

Every stored test the change reaches, also through other functions.

Property tests

And at the edges?

Every defined pure function at 0, ±1, empty values and the bounds of its req; plus the type invariants.

Relink

Does the rest still hold?

Every dependent definition gets a new hash and is checked along.

+ E0807

The behaviour memory: earlier real program runs are replayed. If a define changes their output, the reply names exactly those runs, once, with old and new output.

Try it yourself

The real compiler, here in your browser

The QAL compiler is written in QAL and compiled to WebAssembly. That very module, 444 KB, now runs on your machine. Write code or pick an example: the answer is the same one an agent gets.

Loading the compiler …
Not checked yet

Once the compiler is loaded, it checks as you type.

In the browser run the parser, type checking, effect checking and exhaustiveness of match. Z3 proofs, tests and the store run in the full qal tool.

Everything QAL does

The complete atlas

Every capability of the language, the store and the tools, with what it means for an agent. Compiled from the language reference and qal --help, as of 26 October 2026.

LanguageVerificationStore ExecutionServicesAI calls Standard libraryToolsTeamCompiler
01 · Language

Small, strict, no surprises

Everything is an expression. There is no null, no exceptions, no implicit conversions and no loops.

TypesInt (64-bit), Float, Bool, Unit, Str, Bytes, List[T], Map[K, V] (ordered by key), Option[T], Result[T, E] and function types.
Records and variantsYour own types as a record or as an enumeration with data.type Shape = Circle(Int) | Rect(Int, Int) | Dot
GenericsGeneric types and functions; type arguments are inferred at the call.fn swap[A, B](p: Pair[A, B]) -> Pair[B, A]
Exhaustive pattern matchingPatterns with constants, variants, records and guards. Every match has to cover every case.
ClosuresAnonymous functions that capture their surroundings. Values are immutable; functions are values.map(xs, fn(x) => x * k)
Effects in the typeWhoever reads, writes or goes to the network says so: !io !fs !time !rand !net !db !model. Callers carry the union.
Effect polymorphismA function takes on its callback's effects; with a pure callback it stays pure.fn each[T, !e](xs: List[T], f: fn(T) -> Unit !e) -> Unit !e
Recursion instead of loopsA call in tail position is a loop. Lists are processed with map, filter, fold and range.
Exact integersa * b / c is computed exactly with a 128-bit intermediate. A real overflow and division by zero stop the program instead of computing on wrongly.
Placeholderstodo() stands for a missing body of any type; executed, it stops with E0540.
02 · Verification

Prove, test, remember

Four nets that run with every write: proofs, tests, property tests and the behaviour memory.

Contractsreq is the precondition, ens the postcondition, r the result. They always hold at run time too.fn sqrt_floor(n: Int) -> Int req n >= 0 ens r * r <= n
Z3 proofsExact for Int and Bool, using the contracts of the functions called. Refuted: not stored, with a counterexample. Not provable: unknown with a reason, checked at run time.
Affected testsA define runs every stored test that reaches a changed function, also indirectly.
Edge property testsEvery defined pure function at 0, ±1, empty values and the bounds of its req. Inputs are built so that they satisfy the precondition.
Generated property testsqal_test checks every pure function with an ens on 100 inputs; a failure comes with a shrunk counterexample.
Type invariantsA pure function inv_T is the rule for type T. Every function that takes or returns a T is checked against it, also deep inside lists and records.
Behaviour memory (E0807)Earlier program runs are replayed with every define, up to 64 in 2 s. Changed outputs are reported once and then become the new baseline.
Warning on an untested changeIf a define replaces a function without a test, E0806 warns: every new rule should get a test in the same step.
Memory for correctionsIf an error was fixed before, the new diagnostic names that fix; qal_recall lists earlier corrections.
Proofs by hashResults are stored per definition and hash. What has not changed is not proven again.
03 · Store

Code as addressed nodes

An SQLite store in .qal/store.db. Every definition is kept under the SHA-256 of its canonical form.

Only checked code is storedWhat does not parse or type-check never reaches the store. Every error is a JSON diagnostic with a path and hints.
Replace with relinkingAn existing name is replaced. With the same signature, every user is relinked and re-checked automatically.
Signature changesDependents that still fit come along; the others are rejected with their errors, unless the same call redefines them.
Rename without rewritingqal_rename changes no hash; every user follows the new name.
Safe deletionqal_delete removes only what nothing uses any more.
QueriesBy name, type pattern or users; an outline with contracts, users and tests (--outline).
HistoryEvery change of every name with old and new hash, time and agent.
Incremental checkingOnly what changes is checked and hashed, and the result is byte-identical to the full check. At 1520 definitions that is 0.43 instead of 1.7 s.
PackagesParts of the store can be exported as .qalpkg, imported and installed, from a file or a URL.
Several writersConcurrent writes are queued behind a lock; a proof runs outside the lock meanwhile.
04 · Execution

WebAssembly with fixed limits

Every program is compiled to WebAssembly and runs in Wasmtime, isolated from the system.

SandboxLimits for compute, memory (256 MiB for programs), output and run time. An effect without a grant is not available in the program at all.
Fine-grained grantsfs:<dir> for one directory only, net:<host>[:port] for one host only, db:mem for a fresh in-memory database.qal run main --allow io,fs:data,net:api.example.org
Running programsqal_run starts main(args) with arguments and input; the return value is the exit code.
Calling functions directlyqal_call calls any function with JSON arguments, without writing a main.
Many cases in one callcases runs several inputs in turn, in qal_run and right after a define.
Building a standalone moduleqal build produces the WebAssembly module of a function.
05 · Services

HTTP, database, network

QAL programs can be web services, use SQLite and call other services, with built-in types for all of it.

HTTP handlersA service is a function from request to response; any effects are allowed.fn handle(rq: HttpRequest) -> HttpResponse
HTTP serverqal serve with workers, a queue, timeouts, size limits for request and response, and compute and memory limits per request.
Testing requestsqal_request replays requests against a handler, without a server and without a network.
SQLite with checked SQLdb_exec and db_query take only an SQL literal with ? placeholders, one statement, no PRAGMA or transaction commands. That is enforced when the code is checked.
TransactionsOne transaction per execution; committed only on success, such as status 200 to 399 or exit code 0.
Outgoing callshttp(call) with typed errors (denied, invalid, connection, timeout, too large). Redirects are not followed.
06 · AI calls

Models as a budgeted effect

Programs can ask a language model themselves. It is an effect like any other: declared, granted and limited.

std.modelask returns text, ask_full also the model, tokens and cost, ask_json parsed JSON following a schema.
BudgetEvery call is charged against a fixed budget in euros, rounded up. Once it is used up, ModelBudgetExceeded comes back instead of another call.
RecordingEvery answer is stored by prompt, schema and model. The same question costs nothing the second time.
Deterministic replay--replay plays back only what was recorded, without network and without a key. Tests may ask a model and always see recorded answers only.
07 · Standard library

231 definitions in 7 modules

Present in every project automatically and read-only. Every name is fully qualified, such as std.json.parse.

std.jsonReading, writing and searching JSON; with 77 definitions the largest module.
std.routeRoutes for HTTP services, generic over the result type (38 definitions).
std.strMore string functions beyond the built-in ones (35).
std.http and std.urlHelpers for requests, responses and headers (28), and for splitting and encoding URLs (27).
std.dbConvenient access to rows and columns of database results (22).
std.modelThe model calls from section 06 (4).
Built-in functionsFor strings, lists, maps, bytes, numbers and the system: split, fold, map_put, sort_str, compare, read_line, now_ms, rand_int and more.
08 · Tools

For agents and for people

Agents talk to the store through an MCP server, people through the command line. Both use the same operations.

MCP server with 20 toolsqal_define, qal_test, qal_prove, qal_run, qal_call, qal_view, qal_query, qal_history, qal_rename, qal_delete, qal_build, qal_request, qal_recall and the team tools.
Command lineinit, define, view, query, history, rename, delete, test, prove, run, call, build, serve, request, export, import, install, recall, team, verify.
Checking and formatting filesqal check and qal fmt also work on QAL files outside a store.
Editor supportqal lsp is a language server for editors.
A compact referenceThe language reference comes with the description of qal_define: at most 68 lines, so an agent can read it at every start.
Importing correctionsqal corrections import adds collected corrections to a project's memory.
09 · Team

Several agents, clear roles

A team store lets several agents work together, with roles, change sets and a fully signed history.

Four rolesArchitecture sets interfaces and contracts, implementation fills in bodies, verification writes tests and checks, review reads and approves.
Change setsCode is written only in your own change set; the main line changes only by a merge.
LeasesWhoever writes a name holds it. Another change set gets E0901 with the holder's name.
Merge gateA merge needs "verified" and "approve" from someone other than the owner. It replays the changes, proves afresh and runs every test.
Rebase with conflict marksOn conflicts the main line becomes the new base; conflicting names keep your version with a mark until they are defined again.
Signed historyEvery write is an Ed25519-signed record; qal verify checks the whole chain. Sessions are bound to members.
10 · Compiler

Written in itself

The QAL compiler is written in QAL and compiles itself. A Rust core surrounds it.

Self-hosted17 modules with about 15,000 lines of QAL: lexer, parser, type checker, monomorphisation, SQL checking, encoding and WebAssembly generation.
Bootstrap fixpointStages 1, 2 and 3 of the compiler are byte-identical. That is shown again after every change to the compiler.
Rust referenceAn independent reference compiler in Rust computes in parallel; test suites compare both over a corpus of more than 900 programs.
Parallel checkingLarge programs are split into work items and checked on several cores. CHECK_DELTA checks only the changed bodies against stored signatures.
Rust coreAbout 52,000 lines of Rust for the store, runtime, prover, server and tools, without a single compiler warning.
Diagnostics

Every error has a name

A diagnostic consists of code, kind, definition, path, message and hints. A selection of the codes an agent sees most often:

When writing

CodeMeaning
E0201unknown name
E0202name used twice
E0240reserved name, e.g. from the prelude or std.
E0241 · E0242SQL not a literal, or a statement that is not allowed
E0301effect used but not declared
E0404one definition refers to two names of the same definition
E0508effect not granted when running
E0540todo() was executed
E0801contract refuted; not stored, with a counterexample

Warnings after a define

CodeMeaning
E0803property test failed
E0804property test traps, e.g. overflow or index
E0805an unbounded product can overflow
E0806function changed, but no test in the same step
E0807the output of earlier real runs changed

In a team

CodeMeaning
E0901name is held by another change set
E0905 · E0906outside the work package, or interface changed
E0910 – E0913merge: conflict, does not check, proof or test fails, approval missing
Measured, not claimed

The numbers behind the one round

Every value comes from measurements on 25 and 26 October 2026. The reports are in the repository under bench/.

0.28 smedian of a complete define, 66 functionsbench/loop/report.md
0.41–0.46 sthe same at 1520 definitions, formerly 4.5–5.0 sbench/loop/report.md
0 / 2424differences between incremental and full checkingdifferential test, 318 stores
95 / 96stages with every hidden test green, runs 7–14bench/living
One define, all five checksBeforeNow
66 functions (median)1.24 s0.28 s
1520 definitions4.5–5.0 s0.41–0.46 s
An agent's tokens compared with Rust2.06×1.29–1.32×
A real catch

Every test green, and still a bug

A Haiku agent was asked to add orders with several lines. After its first define, all of its own tests passed. Only the behaviour memory reported that an old one-line order now cost a different amount.

  1. The agent read the warning and concluded: one-line orders must stay the same.
  2. It fixed the discount formula in the next round.
  3. Counter-check: the state before the fix would have failed 5 of 50 hidden tests.

On deliberately planted bugs, E0807 alone, without a single test, reports 11 of 13. In 30 live trials there was no false alarm.

E0807 behaviour_changed
this define changed what `main` prints on 3 of 25 earlier runs: `OK o1 8800` is now `OK o1 8835`
Verbatim from trial 12, commit 9ab47ae8
Why QAL

When an agent writes the code

  • Feedback in one roundAn agent learns at once whether types, contracts, tests and dependents hold. It does not have to plan a build or read logs.
  • Bugs that tests do not seeProofs and the behaviour memory catch what an agent's own tests miss.
  • Controlled effectsEvery effect is in the type and has to be granted. Without --allow model a program cannot call a model or spend money.
  • Answers as dataEvery result is JSON, every error has a code, a path and a hint for the fix.
  • Collaboration without chaosRoles, leases, a merge gate and a signed history make clear which agent changed what.
What is not better yet

Honestly measured

  • CostAgents use about 1.3 times as many tokens in QAL as in Rust. The biggest item is the language reference every agent reads.
  • No time saved per taskOn small programs the faster checking changes rounds and run time measurably not at all. Its value shows on large programs and as a safety net.
  • Proofs with limitsThey are exact for integers and booleans. What Z3 cannot prove is checked at run time.
  • A young languageQAL is measured on an order system with twelve change stages. Broader experience in use is still missing.
Get started

One project, one store, the first round

QAL is built with Cargo. Agents connect through the MCP server; people use the same commands on the command line.

Build 
cargo build --release --manifest-path qal/Cargo.toml -p qal-cli
Create a store and write code 
qal init && qal define account.qal
Run every test and prove a contract 
qal test && qal prove deposit
For agents: start the MCP server in the project 
qal mcp --root .
Run a program as a web service 
qal serve handle --listen 127.0.0.1:8080 --allow db