A programming language

AI writes the implementation, humans and the compiler verify intent.

An AI-collaborative language built for vibe coding.

Every publicly visible function must carry a spec. The spec is the single source of truth — and the intent itself is verified too.

Open the Playground Read the spec

fn max(a: Int, b: Int) -> Int
  spec {
    post result >= a && result >= b
    examples { max(1, 2) == 2 }
  }
{ if a >= b { a } else { b } }

Core invariant

Three rules, enforced at compile time

Visible functions require a spec

Every publicly visible function declares its preconditions, postconditions, and examples where it is defined; a public function without a spec does not compile.

The spec is the single source of truth

Docs, comments, and tests stop drifting apart — requirements live next to the code and are executable.

The spec itself is verified

The compiler checks both directions: the implementation satisfies the spec, and the spec is non-vacuous, consistent, and reachable.

Example

Intent, written into the code

fn max(a: Int, b: Int) -> Int spec { post result >= a post result >= b post result == a || result == b examples { max(1, 2) == 2 max(5, 5) == 5 max(0, -3) == 0 } } { if a >= b { a } else { b } }

Keep editing in the Playground →

Roadmap

Status: M1–M5 complete