Kōdo

The programming language designed for AI agents — transparent for humans.

---

Why Kōdo?

AI agents are writing more and more production code. But the languages they write in were designed decades ago, for humans typing at keyboards. The result: ambiguous code, no correctness guarantees, no way to trace which agent wrote what, and no enforcement that safety-critical code was actually reviewed.

Kōdo is the first compiled language designed from scratch for AI agents to write, reason about, and maintain software — while remaining fully transparent and auditable by humans. It's not a framework, a linter, or a set of conventions bolted onto an existing language. It's a new language where the problems of AI-generated code are solved at the grammar level.

If your team uses AI agents to generate or maintain code, Kōdo gives you what no other language does: contract verification via SMT solver, compiler-enforced authorship tracking, and intent-driven code generation.

The Problem with AI + Existing Languages

Problem	What happens today	What Kōdo does
No correctness guarantees	AI generates code that "looks right" but has subtle bugs	Contracts (requires/ensures) verified by Z3 SMT solver at compile time
No authorship tracking	You can't tell which agent wrote which function	@authored_by, @confidence, @reviewed_by — compiler-enforced
No trust enforcement	Low-quality AI code ships without review	Code below 0.8 confidence won't compile without human sign-off
Ambiguous semantics	AI hallucinates APIs, misunderstands ownership	Zero-ambiguity LL(1) grammar, linear ownership (own/ref), no implicit conversions
Boilerplate generation	AI generates repetitive glue code that rots	Intent blocks: declare what, compiler generates how
Opaque modules	AI generates code without explaining purpose	Mandatory meta blocks — every module is self-describing
Useless error messages	Compiler errors are for humans, not agents	Structured JSON errors with machine-applicable fix patches, Levenshtein suggestions
No repair loop	Agent gets an error, guesses the fix	kodoc fix applies patches automatically — agent reads error, applies fix, recompiles

---

What Makes Kōdo Different

1. Compiler-as-Reviewer: Trust Policies for AI Code

No other language tracks AI vs. human authorship with compiler enforcement. In Kōdo, every function can declare who wrote it, how confident the agent was, and whether a human reviewed it. The compiler uses this to reject unsafe AI code before it ships.

// High confidence — compiles without review
@authored_by(agent:"claude")
@confidence(0.95)fnadd(a:Int,b:Int) -> Int{return a + b
}// Low confidence — won't compile without human sign-off
@authored_by(agent:"claude")
@confidence(0.5)
@reviewed_by(human:"rafael")
fn experimental(a:Int, b:Int) -> Int{
return a * b
}// Security-sensitive — won't compile without contracts
@security_sensitive
fn safe_divide(a:Int, b:Int) -> Intrequires{ b != 0}{return a / b
}

Confidence propagation is transitive: if function A (confidence 0.95) calls function B (confidence 0.5), A's effective confidence drops to 0.5. You can't hide low-quality code behind a high-confidence wrapper. kodoc confidence-report visualizes the entire call graph with effective confidence scores.

Enforced policies:

• @confidence below 0.8 → @reviewed_by(human: "...") required, or compilation fails (E0260)
• @security_sensitive → at least one requires/ensures contract required (E0262)
• min_confidence in module meta → all functions must meet the threshold (E0261)

2. Contracts as Grammar — Verified by Z3 Before Code Runs

Contracts aren't comments, decorators, or type annotations — they're part of the language syntax, verified by the Z3 SMT solver at compile time. The compiler doesn't just catch type errors; it catches logical errors.

fnsafe_divide(a:Int,b:Int) -> Intrequires{ b != 0}{return a / b
}fnclamp(value:Int,min:Int,max:Int) -> Intrequires{ min <= max }{if value < min {return min }if value > max {return max }return value
}

Why this matters for AI agents: an agent doesn't just generate code — it generates code with mathematical proof of correctness. When an agent writes requires { b != 0 }, the compiler verifies it at every call site. Bugs that would survive code review in other languages are caught at compile time.

3. Error Messages Designed for Machines (and Humans)

In most languages, error messages are formatted for humans. AI agents have to parse free-text output, guess what went wrong, and hope their fix is right. Kōdo's compiler is designed for agent consumption:

# Structured JSON with machine-applicable patches
kodoc check file.ko --json-errors

{
"code": "E0201",
"message": "undefined type `conter`",
"suggestion": "did you mean `counter`?",
"fix_patch": {
"description": "rename to closest match",
"start_offset": 42,
"end_offset": 48,
"replacement": "counter"
}
}

# Automatic error correction — no guessing
kodoc fix file.ko

What the compiler gives agents:

• Unique error codes (E0001–E0699) with structured JSON — no regex parsing needed
• Levenshtein-based suggestions — "did you mean counter?" for typos (E0201)
• Machine-applicable fix patches — byte offsets + replacement text, apply without interpreting prose
• kodoc fix — applies all patches automatically, creating a compile→fix→recompile loop
• Complete explanations — kodoc explain E0240 gives full context for any error code

This creates a closed-loop repair cycle: agent writes code → compiler returns structured error → agent applies fix patch → recompile. No ambiguity, no guessing.

4. Intent-Driven Programming

Declare what you want. The compiler generates how.

module intent_demo{
meta {purpose:"Demonstrates intent-driven programming in Kōdo",version:"1.0.0"}
intent console_app{greeting:"Hello from intent-driven Kōdo!"}}

No main(), no boilerplate. The intent block is a declaration of intent — the compiler expands it into concrete code at the AST level with full type checking. Think of it as a semantic macro, not a text substitution.

Why this matters for AI agents: less generated code = fewer bugs. The agent declares intent ("I want a console app that prints X") and the compiler guarantees the implementation is correct. Inspect what any intent generates with kodoc intent-explain.

5. Linear Ownership — Correct by Construction

Kōdo enforces linear ownership at the type level. Every value has exactly one owner. When a value is moved, it cannot be used again. Borrow with ref to share without transferring ownership. Use mut for exclusive mutable access — no other borrows may coexist.

fnconsume(own s:String){println(s)}fnborrow(ref s:String){println(s)}fnmain(){let msg:String = "hello"
borrow(msg)// OK — msg is borrowed, still usable
borrow(msg)// OK — msg is still ownedconsume(msg)// OK — msg is moved to consume// println(msg) // E0240: use-after-move}

Copy semantics for primitives:Int, Bool, Float, Byte are implicitly copied — only compound types (structs, strings) enforce move semantics. This eliminates false positives without sacrificing safety.

Why this matters for AI agents: agents frequently generate code with aliasing bugs, dangling references, and use-after-free. Kōdo catches these at compile time with clear, structured error messages that the agent can fix automatically.

6. Self-Describing Modules

Every Kōdo module must include a meta block. The compiler rejects code without it.

module payments{
meta {purpose:"Process recurring subscription payments",version:"2.1.0"}// ...}

AI agents and humans can understand any module's purpose without reading the implementation. Self-documentation isn't optional — it's enforced at the grammar level.

---

A Complete Language

Kōdo isn't just annotations on top of another language — it's a full compiled language with native binary output via Cranelift:

Category	Features
Type system	Int, Float64, Bool, String, structs, enums, tuples ((Int, String)), generics with monomorphization and trait bounds (<T: Ord + Display>), dyn Trait (dynamic dispatch with vtables), local type inference, no implicit conversions
Pattern matching	Exhaustive match on enums with destructuring, short variant patterns (Ok(v), Some(v) without enum prefix)
Testing	Built-in test blocks, describe grouping with setup/teardown, @skip/@todo/@timeout annotations, @property + forall property-based testing with basic shrinking, kodoc generate-tests for contract-driven stub generation, kodoc test --json for agent consumption
Closures	Lambda lifting, capture analysis with ownership tracking (E0281–E0283), higher-order functions, (Int) -> Int types
Ownership	Linear ownership (own/ref/mut), Copy semantics for primitives, use-after-move (E0240), borrow-escapes-scope (E0241), move-while-borrowed (E0242), mut-borrow-while-ref-borrowed (E0245), ref-borrow-while-mut-borrowed (E0246), double-mut-borrow (E0247), assign-through-ref (E0248), closure capture ownership (E0281–E0283), atomic reference counting (thread-safe automatic deallocation)
Contracts	requires/ensures verified by Z3 SMT solver, runtime fallback, recoverable mode, module-level invariant blocks
Agent traceability	@authored_by, @confidence, @reviewed_by, transitive confidence propagation, min_confidence threshold
Error repair	Machine-applicable FixPatch in JSON, multi-step RepairPlan for complex errors, kodoc fix for auto-correction, Levenshtein suggestions for typos
Error handling	Option<T> and Result<T, E> in the prelude, ? operator for Result propagation — no null, no exceptions
Bare constructors	Ok(v), Err(e), Some(v), and None work without Result::/Option:: prefix — desugared by the type checker and MIR lowering into existing enum variant representation
String interpolation	f"Hello {name}!" — f-strings desugar to concatenation with automatic to_string
Inherent impl blocks	impl Point { fn distance(self) ... } — methods on structs without requiring a trait
Iterators & functional	Iterator protocol for List<T>, String, Map<K,V>, Set<T>; functional combinators (map, filter, fold, reduce, count, any, all); functional pipelines
Standard library	abs, min, max, clamp, string methods (length, contains, split, trim, to_upper, to_lower, substring, concat, index_of, replace, lines, parse_int), List<T> (push, get, pop, remove, set, slice, sort, join), Map<K,V> (Int and String keys), Set<T> (add, contains, remove, union, intersection, difference), methods on Option<T> and Result<T,E>, generic method dispatch, File I/O (file_read, file_write, file_append, file_delete, file_exists, dir_list, dir_exists), HTTP client (http_get, http_post returning Result<String, String>), HTTP server (http_server_new, http_server_recv, http_request_method/path/body, http_respond), JSON (json_parse, json_get_string, json_get_int, json_free, json_new_object, json_set_string/int/bool, json_stringify), CLI (args, readln, exit), Math (sqrt, pow, sin, cos, log, floor, ceil, round, rand_int), Regex (regex_match, regex_find, regex_replace)
Visibility	pub fn, pub struct — declarations are private by default, pub makes them accessible from other modules
Multi-file	import module_name across .ko files, selective imports (import math { add, Point }), qualified calls (math.add(1, 2))
Concurrency	Green threads with M:N work-stealing scheduler, spawn on green threads (64KB stacks), async/await with Future<T>, parallel {} with OS threads, generic Channel<T> for any type, actor with state and message passing, cooperative yield points at loops and calls, --threads=N configuration
Developer tools	Interactive REPL (kodoc repl) with full compile-and-execute pipeline and persistent history (~/.kodo_history); LSP server with diagnostics, hover (full annotations), goto-definition (functions, variables, params, structs, enums), find-references (with include_declaration), contract-aware completions (31 builtins), and code actions from FixPatch; VSCode extension for seamless editor integration; Neovim plugin with syntax highlighting, indentation, and LSP support (setup guide); tree-sitter grammar for advanced syntax highlighting (tree-sitter-kodo); MCP server (kodo-mcp) with 7 tools including kodo.annotate for agent-driven contract inference via JSON-RPC over stdio; kodoc annotate --ai for LLM-assisted contract suggestion; JSON error output; kodoc explain for any error code; kodoc audit for consolidated trust reports
Package manager	kodoc init (scaffold project with kodo.toml + src/main.ko), kodoc add (git or path dependencies), kodoc remove, kodoc update (re-resolve and update kodo.lock)
Build artifacts	Compilation certificates (.ko.cert.json) with SHA-256 hashes, per-function confidence scores, per-function contract status (static_verified/runtime_only/no_contracts), and contract verification stats

---

Performance

Benchmark	Kōdo (Inkwell)	Kōdo (Cranelift)	Rust	Go	Python
fib(35)	0.029s	0.035s	0.04s	0.09s	0.87s
sum 10M	0.020s	0.022s	0.00s	0.08s	0.48s

Kōdo with the Inkwell (LLVM) backend is faster than Rust on recursive workloads and 4x faster than Go on tight loops. Concurrency-aware yield analysis skips overhead for pure functions — no unnecessary scheduling in computational code.

Two backends: Cranelift (default, fast compilation) and Inkwell (LLVM C API, --release flag, maximum runtime performance).

---

Quick Start

Option A: Download Pre-Built Binary

Download the latest release from the Releases page:

# macOS (Apple Silicon)
curl -L https://github.com/rfunix/kodo/releases/latest/download/kodoc-macos-aarch64 -o kodoc
# Linux (x86_64)
curl -L https://github.com/rfunix/kodo/releases/latest/download/kodoc-linux-x86_64 -o kodoc
chmod +x kodoc
sudo mv kodoc /usr/local/bin/

Option B: Build from Source

Prerequisites:Rust toolchain (1.91+) and a C linker (cc).

git clone https://github.com/rfunix/kodo.git
cd kodo
make install

This builds in release mode and installs kodoc to ~/.kodo/bin/. Add to your PATH:

echo'export PATH="$HOME/.kodo/bin:$PATH"'>>~/.zshrc
source~/.zshrc

Verify:

kodoc --version

Hello World

Create hello.ko:

module hello {
meta {purpose:"My first Kōdo program",version:"0.1.0",author:"Your Name"}fnmain(){println("Hello, World!")}}

Compile and run:

kodoc build hello.ko -o hello
./hello

Or try the interactive REPL:

kodoc repl
# kōdo> println("Hello from the REPL!")# kōdo> let x: Int = 2 + 3# kōdo> fn double(n: Int) -> Int { return n * 2 }# kōdo> double(x)

---

Examples

The examples/ directory contains 150 compilable programs:

Core Language

File	What it demonstrates
hello.ko	Minimal hello world
fibonacci.ko	Recursive functions
while_loop.ko	Loops and mutable variables
structs.ko	Struct definition and field access
struct_params.ko	Structs as function parameters and return values
enums.ko	Enum types and pattern matching
enum_params.ko	Enums as function parameters
expressions.ko	Arithmetic and boolean expressions
for_loop.ko	For loop iteration
optional_sugar.ko	Optional syntactic sugar (?., ??)
break_continue.ko	Break and continue in loops
type_errors.ko	Demonstrates type error messages
type_inference.ko	Local type inference for let bindings

Type System

File	What it demonstrates
generics.ko	Generic enum types
generic_fn.ko	Generic functions with monomorphization
option_demo.ko	Option<T> — no null values
result_demo.ko	Result<T, E> — explicit error handling
result_bare_constructors.ko	Bare Ok/Err/Some/None constructors without Result::/Option:: prefix
try_operator.ko	Result pattern matching for error handling
flow_typing.ko	Flow-sensitive type narrowing
traits.ko	Trait definitions and static dispatch
generic_bounds.ko	Generic trait bounds (<T: Ord>)
sorted_list.ko	Bounded generics with sorted collections
advanced_traits.ko	Advanced trait patterns
associated_types.ko	Associated types in traits
methods.ko	Inherent impl blocks — struct methods
tuples.ko	Tuple types, literals, indexing, and destructuring

Functions & Closures

File	What it demonstrates
closures.ko	Closures and direct closure calls
closures_functional.ko	Higher-order functions and indirect calls
float_math.ko	Float64 arithmetic operations
string_concat_operator.ko	String concatenation with + operator
string_interpolation.ko	F-string interpolation (f"Hello {name}")
stdlib_demo.ko	Standard library: abs, min, max, clamp
regex_demo.ko	Regex builtins: regex_match, regex_find, regex_replace

Contracts, Ownership & AI Traceability

File	What it demonstrates
contracts.ko	Basic contract syntax
contracts_demo.ko	Runtime contract checking (requires/ensures)
contracts_verified.ko	Statically verified contracts via Z3
contracts_smt_demo.ko	SMT solver contract verification demo
smt_verified.ko	SMT contract verification
recoverable_contracts.ko	Recoverable contract mode (--contracts=recoverable)
ownership.ko	Linear ownership with own/ref, move semantics for structs
borrow_rules.ko	Borrow rules: multiple ref borrows, mut exclusivity
move_semantics.ko	Move semantics, Copy vs non-Copy types
copy_semantics.ko	Implicit Copy for primitives vs move for compounds
confidence_demo.ko	Transitive confidence propagation through call graph
agent_traceability.ko	@authored_by, @confidence, @reviewed_by, @security_sensitive
refinement_types.ko	Refinement types with requires constraints
refinement_smt.ko	SMT-verified refinement types
struct_predicates.ko	Struct field predicates in contracts
memory_management.ko	Reference counting for heap-allocated values
module_invariant.ko	Module-level invariant blocks for global properties
visibility.ko	pub/private visibility for functions and structs

Intent System

File	What it demonstrates
intent_demo.ko	Intent-driven programming (console_app)
intent_math.ko	Math module intent resolver
intent_composed.ko	Multiple intents composed in one module
intent_http.ko	HTTP intent resolver
intent_database.ko	Database intent resolver
intent_json_api.ko	JSON API intent resolver
intent_cache.ko	Cache intent resolver
intent_queue.ko	Queue intent resolver
intent_cli.ko	CLI tool intent resolver
intent_http_server.ko	HTTP server intent resolver
intent_file_processor.ko	File processor intent resolver
intent_worker.ko	Worker loop intent resolver

Collections & I/O

File	What it demonstrates
list_demo.ko	List<T> — list_new, list_push, list_get, list_length, list_contains
map_demo.ko	Map<K,V> — map_new, map_insert, map_get, map_contains_key, map_length
set_operations.ko	Set<T> — Set::new, add, contains, remove, length, union, intersection, difference
map_string_string.ko	Map<String, String> — generic map with String keys and values
map_string_int.ko	Map<String, Int> — generic map with String keys
map_int_string.ko	Map<Int, String> — generic map with String values
string_demo.ko	String methods including split, trim, to_upper, substring
for_in.ko	For-in loops over List<T> collections
file_io_demo.ko	File I/O: file_exists, file_read, file_write
http_client.ko	HTTP GET with Result<String, String>
time_env.ko	Time functions and environment variables
cli_args.ko	Reading command-line arguments with args()
json_builder.ko	JSON construction: json_new_object, json_set_*, json_stringify
math_demo.ko	Extended math: rand_int
http_api.ko	HTTP server with JSON responses via tiny_http

Iterators, Functional Combinators & Methods

File	What it demonstrates
iterator_basic.ko	Basic iterator protocol
iterator_list.ko	Iterating over List<T>
iterator_string.ko	Iterating over String characters
iterator_map.ko	Iterating over Map<K,V> entries
iterator_map_filter.ko	map and filter combinators on iterators
iterator_fold.ko	fold combinator for aggregation
functional_pipeline.ko	Functional pipelines with chained combinators (map/filter/fold/count/any/all)
enum_methods.ko	Methods on Option<T> and Result<T,E> enum types
generic_method_dispatch.ko	Generic method dispatch on parameterized types

Real-World Examples

File	What it demonstrates
todo_app.ko	Agent-built task manager with @authored_by, @confidence, forced @reviewed_by, contracts
config_validator.ko	Config validation with refinement types (Port, MaxConns), @security_sensitive, module invariant
health_checker.ko	Health checker with file_exists, fold aggregation, --json-errors for agent consumption
url_shortener.ko	URL shortener with @security_sensitive, contracts, Map<Int,Int> lookup
word_counter.ko	Word counter demonstrating ref borrowing (E0240 prevention), for-in over .split()
audit_log/	Multi-file audit log: 15+ features (contracts, refinement types, agent traceability, functional pipelines, enums, pattern matching, multi-file imports)
self_hosted_lexer/	Self-hosted lexer: a Kodo tokenizer written in Kodo itself — proves language expressiveness for compiler work

Concurrency & Multi-File

Note:spawn with captured variables, actor with state/message passing, parallel blocks, channels, and async/await with thread pool runtime are fully working.

File	What it demonstrates
async_demo.ko	async fn / await — real green-thread concurrency
async_real_demo.ko	Two concurrent async tasks, both awaited
async_real.ko	Cooperative spawn syntax preview
async_tasks.ko	Spawn with captured variables
concurrency_demo.ko	Concurrency patterns
actors.ko	Actor state and message passing
actor_demo.ko	Actor demonstration
parallel_blocks.ko	Structured concurrency with parallel blocks
channels.ko	Inter-thread communication with channels
channel_string.ko	Generic typed channels
parallel_demo.ko	Structured concurrency with parallel {} and async runtime
qualified_imports.ko	Qualified imports (math.add(1, 2))
selective_imports.ko	Selective imports (import { add } from math)
send_sync_demo.ko	Send/Sync bounds for thread safety
multi_file/	Multi-file compilation with imports

Vericoding Benchmark

The bench/vericoding/ directory contains 20 formally verified programs equivalent to the AlgoVeri benchmark (77 algorithms in Dafny/Verus/Lean). Each task has:

• A JSON spec with description, signature, and expected output
• A Kōdo solution with requires/ensures contracts verified by Z3

cd bench/vericoding && ./run.sh --verbose # run all 20 tasks
./run.sh --json # JSON output for CI

Result: 20/20 tasks passing (100% success rate).

---

Compiler Architecture

Source (.ko)
│
▼
┌─────────────┐
│ kodo_lexer │ Token stream (logos-based DFA)
└──────┬──────┘
▼
┌─────────────┐
│ kodo_parser │ AST (hand-written recursive descent, LL(1))
└──────┬──────┘
▼
┌─────────────┐
│ kodo_types │ Type checking (no inference across modules)
└──────┬──────┘
▼
┌──────────────────┐
│ kodo_contracts │ Z3 SMT verification (static) + runtime fallback
└──────┬───────────┘
▼
┌────────────────┐
│ kodo_resolver │ Intent expansion (intent blocks → concrete code)
└──────┬─────────┘
▼
┌──────────────┐
│ kodo_desugar │ Syntactic desugaring (for loops, optional sugar)
└──────┬───────┘
▼
┌─────────────┐
│ kodo_mir │ Mid-level IR (CFG, basic blocks)
└──────┬──────┘
▼
┌─────────────────┐
│ MIR Optimizer │ Constant folding, DCE, copy propagation
└──────┬──────────┘
▼
┌──────────────┐
│ kodo_codegen │ Native binary (Cranelift)
└──────────────┘

13 crates in a Rust workspace. Zero circular dependencies. Zero clippy warnings.

---

Documentation

• Documentation Index — start here
• A Tour of Kōdo — quick walkthrough of all features
• Getting Started — install, build, run
• Language Basics — modules, functions, types, variables, control flow
• Data Types and Pattern Matching — structs, enums, and match
• Pattern Matching — exhaustive match on enums
• Generics — generic types and functions
• Traits — trait definitions and static dispatch
• Inherent Methods — struct methods without traits
• Error Handling — Option<T> and Result<T, E>
• Contracts — requires and ensures
• Ownership — linear ownership with own/ref
• String Interpolation — f-strings with {expression} embedding
• Agent Traceability — confidence propagation and trust policies
• Closures — closures, lambda lifting, and higher-order functions
• Modules and Imports — multi-file programs and standard library
• HTTP & JSON — HTTP client and JSON parsing
• Actors — actor model with state and message passing
• Concurrency & Spawn — spawn with captured variables
• Real-World Examples — complete programs showcasing agent features
• Intent System — intent-driven programming
• CLI Reference — all kodoc commands and flags
• Language Design — full specification
• Error Index — all error codes

---

Contributing

See CONTRIBUTING.md for development guidelines.

cargo fmt --all # Format
cargo clippy --workspace -- -D warnings # Lint
cargo test --workspace # Test
make ui-test # Run UI tests
make validate-docs # Validate documentation examples
make validate-everything # Run ALL validation phases (fmt, clippy, test, ui-test, docs, examples, CLI)

License

MIT