Your AI writes the code. The compiler proves it.
Edda is a compiled language for codebases written by AI. Every function carries contracts the compiler proves on every build, and every build emits a map of the whole project that your agent reads instead of guessing. The mistake that would have passed code review dies at the build.
Working with an AI agent? The machine-readable setup recipe is /get-started/agent.txt.
function non_negative(x: i64) -> i64
requires x >= 0
ensures result >= 0Delete the requires line and edda build rejects the program, handing you the exact input that breaks it. Put the line back and it builds. Most languages would have shipped the broken version.
Your agent reads the map, not the codebase
Every edda build writes an index.toon file into each source directory: the type checker's own record of every signature, effect, contract, and call edge in it. No human writes it, so it can never drift from the code. Here is the real one sitting beside the standard library's sorter:
loc: src
functions[4]{name,file,line,end,visibility,stability,sig,eff,cone,calls}:
sort.sort_i64,sort.ea,5,8,public,,"(slice: mutable [i64]) -> ()",,=,quicksort_i64 | slice.len
sort.quicksort_i64,sort.ea,10,21,module,,"(slice: mutable [i64], lo: usize, hi: usize) -> ()",,=,partition_i64 | quicksort_i64
sort.partition_i64,sort.ea,23,67,module,,"(slice: mutable [i64], lo: usize, hi: usize) -> usize",,=,slice.len
sort.is_sorted_i64,sort.ea,69,81,public,,"(slice: [i64]) -> bool",,=,slice.len
invariants[4]{target,file,line,rule}:
sort.quicksort_i64,sort.ea,11,decreases (hi - lo)
sort.partition_i64,sort.ea,24,requires (lo < hi)
sort.partition_i64,sort.ea,25,ensures (result >= lo)
sort.partition_i64,sort.ea,26,ensures (result <= hi)Edda's own compiler is 197,000 lines of source across 770 directories; the maps for all of it total 20,000 lines, a tenth the size. Your agent reads the map for the directory it is changing, then opens only the spans it needs. Doc generators summarize comments — this is the type checker publishing what it proved. The design page shows how the maps stay truthful; the tooling page covers the compiler daemon your agent queries directly.
What the compiler guarantees
Each of these is checked on every build. The compiler enforces them, so nobody has to remember.
Provably wrong code does not build
Contracts, integer overflow, array bounds, and division by zero are all proven by a solver during the build. A failed proof names the exact input that breaks the claim.
The docs are compiler output
The map above is regenerated from checked facts on every build. Edda has no comments at all: what you read is what the type checker proved, as current as the code itself.
Refactors land whole or not at all
The compiler runs as a daemon holding the checked project in memory; your editor talks to it over LSP, your agent over MCP. A rename targets a qualified name and rewrites every use, or touches nothing.
Every function declares what it can see and touch
To read a file, a function must be handed the filesystem. To dial out, a dependency must be passed a Network capability by your code. The signature is the audit.
No task outlives its scope
Every task handle ends in exactly one of await, cancel, or detach, and a scope waits for all of its children before it returns. Fire-and-forget does not compile.
Where edda is today
We are bootstrapping a language with itself. The compiler is written in edda, and it type-checks its own 197,000-line source through its own backend; a Rust bootstrap compiler builds it today and defines the reference behaviour while the self-hosted compiler matures.
Windows (x86-64) is the platform we build and test on today; Linux and macOS releases are rolling out through CI. The site you are reading is rendered by a verified edda program.
The compiler, the 24,000-line standard library, the 28,000-line package ecosystem, and the 165,000-line Rust bootstrap were all written by LLM agents working against the compiler's own checks. There was no edda to train on. When the self-hosted compiler retires the bootstrap, the entire toolchain becomes edda, proven by edda.
Build it in edda
Web services & APIs
Ship handlers that list every failure they can raise, on a server that takes its socket as a capability through main. Its entire reach is written in one signature.
Command-line tools
Build one static binary with no runtime to install. The entry signature lists every file, socket, and process the tool can ever reach.
Embedded & firmware
Target bare metal with no garbage collector and no hidden allocations. Memory bounds live in the signature, proven at build time, with layout exact to the wire.
WebAssembly & the edge
Compile to a sandbox that already agrees with the language: a module's imports are the parameters of its main function, so the host grants exactly what the code declares.
Get involved
Read the design — how the language is built up, one decision at a time.
Contribute — the compiler, standard library, and this site are developed in the open.
Join r/EddaLang — questions, showcases, and release threads; or write to ea@edda-lang.org.