From zero to a verified program

The short path

If your agent can browse the web, you barely have to do anything. Say this to it:

I want to use the Edda language — edda-lang.org

It finds the site, reads its own setup at /get-started/agent, places the reference for your harness, and asks you about the optional guardrails before touching your project. The rest of this page is the same journey, done by hand — read on if you'd rather understand each step.

Why there's a setup step

Edda isn't in any model's training data. So the one trick that makes everything work is having your agent read the language reference (AGENTS.md) before it writes a line — after that, the compiler checks its work. You don't change your workflow; you add one file your agent reads, and optionally switch on some guardrails. These steps shrink over time: prebuilt toolchains are landing, and models will eventually see edda.

Choose your harness

Every major coding agent loads a project context file automatically. The only per-tool difference is which file it reads and whether it can run the optional reading-discipline hooks. Edda works with all of them — pick the one you already use.

Not on the list? Drop AGENTS.md at your repo root — it's the cross-tool standard 30+ agents already read. The per-tool file above just makes your agent load it every session; the agent setup page has the exact snippet, and your agent can place it itself.

Choose your model

This choice matters more than the harness. Because edda isn't in training data, your agent works from the reference it just read, not from memory — and that rewards raw capability. Use your harness's strongest, current model, not its fast or mini tier.

A frontier model reads AGENTS.md once and writes correct edda; a small model guesses Rust- or Swift-shaped syntax and then fights the compiler over it. Edda's own compiler, standard library, and this website are all written this way — by top-tier models reading the same reference you're about to hand yours.

Rule of thumb: if your harness offers a "thinking", "pro", or flagship tier, use it here. The ten-minute loop below assumes a capable model — a weak one will still work, but it'll take more turns.

1. Install the toolchain

One line installs a self-contained toolchain — the edda binary, its LLVM runtime, and a vendored std and runes. No Rust, no LLVM, no Z3 to install, and no environment variables to set — just a system linker (MSVC Build Tools on Windows, lld/mold on Linux, the Xcode Command Line Tools on macOS).

Windows (PowerShell)

irm https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.ps1 | iex

Linux / macOS

curl -fsSL https://raw.githubusercontent.com/edda-lang/edda-bootstrap/main/install.sh | bash

The installer downloads the archive for your platform, unpacks it, and puts edda on your PATH. Confirm it with edda version.

Platform status: Windows (x86-64-windows-msvc) is available now and is the verified platform. Linux and macOS archives are still rolling out through CI — until yours lands the installer reports "no release asset for <platform>"; in the meantime build the reference compiler from source (see the edda-bootstrap README) and point EDDA_STDLIB_ROOT at a checkout's std. If you're on Linux or macOS, your bug report (or "it worked") is the most useful thing you can send back.

2. Create a project

A package is a package.toml plus a src/ directory. Make a small but real one — one capability, one contract — so the very first build proves something.

package.toml

[package]
name = "hello"
version = "0.1.0"
root_namespace = "hello"

[build]
default_target = "x86-64-linux-gnu"    # your host: x86-64-windows-msvc, aarch64-macos-darwin, ...

src/main.ea

module hello.main

import std.io.stream

function non_negative(x: i64) -> i64
    requires x >= 0
    ensures result >= 0
{
    return x
}

public function main(out: Stdout) -> ()
    with {out}
{
    let y = non_negative(7)
    out.print_line(f"non_negative(7) = {y}")
}

Every capability main may use is named in its signature — this program holds only Stdout, so it can only print. The requires and ensures clauses are a contract the compiler checks at build.

3. Build and run

From the project directory, edda run prints:

non_negative(7) = 7

4. Break it — watch the build refuse

This is why edda exists. Delete the requires x >= 0 line from non_negative and build again. The compiler refuses — and hands you the exact input that breaks the contract:

error[refinement_unproven]: ensures clause 0: (result >= 0)
 --> src/main.ea:5:5
    note: counter-example:
    note:   result = -1
    note:   x = -1

Without the precondition, the function can no longer guarantee a non-negative result — the solver finds x = -1 and rejects the program before it ever runs. An agent-introduced bug that violates a contract fails the build with a concrete counter-example, not a runtime surprise. Put the line back — and keep this directory as a reusable, contract-verified starter for your next edda project.

Optional: reading-discipline hooks

Edda ships two small hook scripts that make one habit mechanical: read the compiler's structure map (index.toon) for a directory before editing its source, and don't read whole oversized files at once. They keep an agent grounded on a large codebase and cut wasted tokens — and they're portable to every harness in the table above, not just Claude Code.

They're opt-in. Your agent will explain them and ask before installing anything; you can read the scripts first — toon_gate.py is about forty lines. Setup per harness is on the agent setup page.

Hand it to your agent

The point of edda is that your agent writes it. Once the reference is in place, paste this:

Read AGENTS.md (the edda language reference). Then build me <what you
want> in edda, in this project. Run `edda build` after every change and
fix exactly what it reports — the build is the source of truth.

AGENTS.md is the canonical, agent-facing language reference; /get-started/agent is the full self-setup your agent can follow on its own. Edda isn't in most models' training data, so reading the reference first is what makes the loop work.

Next

Read the language pages, learn why the build refuses bad code at verification, and see how to help at contribute. The source lives at edda-lang/edda and edda-lang/edda-bootstrap.