Allegro

Verified code at AI velocity.

Allegro is a programmable language platform where every claim about your code resolves to a proof strength you can see — and where humans and AI agents ship through the same verifying kernel. Everything it does differently is a composition of three moves:

Everything is a value under one engine. Code, types, grammars, proofs, and effects are ordinary values; partial evaluation is the only engine. Type checking, proof discharge, and optimization are not separate passes — they are the same evaluation, run as far as the available facts allow.
Every claim carries a visible strength. There is no boolean "verified" anywhere in the system. A claim — a refinement, a contract, a law, an effect declaration — resolves to a tier: proven, enumerated, sampled, witnessed, admitted, pending. The escape hatches are legal and loud: you may assume a law you can't prove, and everything resting on the assumption says so in its verdict.
Every participant goes through the same kernel. A human, an LLM, a tool — all get the same obligations, propose through the same protocol, and are verified by the same kernel, with authorship recorded per discharged proof. Trust attaches to the kernel's verdict, not to who wrote the code.

A consequence worth naming: code stops being the artifact you review. Refinements, invariants, contracts, effects, and laws accumulate facts the compiler proves; the same facts surface as a semantic summary — types, predicates, contracts, effect sets, safety grade — that humans and AIs review instead of reading line-by-line.

Allegro is a work in progress. The examples below are live — edit them and click Run to evaluate. Click Inspect on any sandbox to see the same code as a structured summary: types, predicates, contracts, safety grade. Open the full sandbox for a richer experience.

Provability — the headline example

A small banking API demonstrates the four layers of Allegro's provability arc working together: a refinement type, arithmetic propagation, a function contract with requires and ensures, and runtime safety where static proof falls short.

Click Run to evaluate

The five layers, each with its own playable example. The first four are the positive aspect of provability — what the code does. The fifth is the negative aspect — what it doesn't do.

Refinement types & domain propagation — facts attached to values flow through arithmetic.
Asserts — universal in-scope predicates, discharged statically when the compiler can prove them.
Lifecycle invariants — predicates that hold for every value of a type, checked on construction.
Contracts — requires / ensures on functions, surfacing in the safety summary.
Effects — what categories of side effects each function can produce; declared and verified against inference.

Constrain existing types with predicates using & (compound predicate bodies compose with &&). The _ placeholder is the value. Construction and call-site checks fire automatically; the recognised algebraic shape (intervals, equality, inequality) propagates through arithmetic so downstream values inherit the proof.

Asserts

Activate use invariants for a universal assert statement. The predicate is checked against the binding's accumulated facts: if entailed, the runtime check disappears and the proven fact joins the binding's predicate set. If not, a runtime check fires and a failed assert halts visibly with a counterexample (no silent error values — build safety in).

Click Run to evaluate

Lifecycle invariants

Lifecycle invariants are ordinary refinements — the & mint covers scalars and records alike. Chained & clauses each form their own layer, so a failure reports the violated clause's constraint with a counterexample. Record predicates reference fields through _.

Click Run to evaluate

Contracts: `requires` & `ensures`

Function bodies declare contracts at the head. requires P is a caller obligation; ensures P is an implementer guarantee, with _ referring to the return value. Predicate-set entailment short-circuits both runtime checks; the post-condition attaches to the result so callers see the proven fact.

Click Run to evaluate

Effects — the negative aspect

Each function can declare which categories of side effects it produces — io, net, time, … — via an effects body clause. The analyzer infers the actual set from the primitives transitively called and verifies the declaration is a superset (under-promising halts compilation). Click Inspect to see the inferred and declared sets surface in the safety summary.

Effect labels are extensible, not a fixed enum. Core ships only the implicit pure; the standard library registers io alongside print, net alongside fetch, and so on. Domain-specific extensions can register their own labels (build-io, funds-mutation, …).

Click Run to evaluate

Try editing the square function to add a print(x) call without removing effects pure — running halts with an effects-mismatch error pointing at the undeclared io effect.

Laws — every claim carries its strength

There is no boolean "verified" in Allegro. Every law obligation — reflexivity, symmetry, transitivity of an equality; algebraic laws you declare on your own types — resolves to a tier: kernel, enumerated, sampled, witnessed, admitted, or pending. Proofs record which tier backed them, and the verdict renders anything weaker than proof loudly.

// Kernel equalities are auto-proven: transitivity over Int is backed
// at tier `kernel`, and the proof value says so.
theorem t_int: 1 == 1 by proof_trans(proof_refl(1), proof_refl(1))
p = proof_trans(proof_refl(7), proof_refl(7))
print(p.lawTier)                 // kernel

// A custom equality: Cell draws Equatable and supplies its own eq.
// Its refl/sym/trans obligations are RECORDED as pending — never
// silently granted.
Cell = Type.define({x: Int, eq: (self, other) => self.x == other.x}, Equatable)
v = Cell(1)

// The strict gate: proof_trans over Cell values is REFUSED while
// Cell's transitivity is neither proven nor admitted. (Try it: move
// the theorem below above the Law.assume line.)

// The escape hatch is legal — and loud:
Law.assume(Cell, "trans")

theorem t_cell: v == v by proof_trans(proof_refl(v), proof_refl(v))
q = proof_trans(proof_refl(v), proof_refl(v))
print(q.lawTier)                 // admitted — nothing upgraded for free

// Or do it properly — witness a real proof:
Cell2 = Type.define({x: Bool, eq: (self, other) => self.x == other.x}, Equatable)
Law.witness(Cell2, "refl", prove_for_all_bool(b => b == b))
print("laws carry their strength")

Click Run to evaluate

Running allegro verify on this file renders the full picture — the admitted obligation marked !, the pending ones ?, a weakness note on every proof resting on the assumption, and the assumption ledger: every assumption in force, mapped to the proofs resting on it. The backing set is transitive — wrap the chain in another combinator and the note survives:

Verdict (verified): 4/4 discharged
  ✓ t_int — by auto-PE
  ✓ t_cell — by auto-PE [resting on admitted 'trans' of 'Cell']
  laws: 13/18 discharged, 1 ADMITTED (assumed, not proof), 4 pending
    ! Cell.trans (admitted)
    ? Cell.refl
    ? Cell.sym
  assumption ledger: rests on 1 admitted, 0 sampled; 4 obligation(s) pending
    ! admitted 'trans' of 'Cell' — backs: t_cell, q

The prover loop — one protocol, any participant

Verification is a loop, and it is participant-neutral: the kernel emits obligations, any prover — an LLM, a human, a tool — proposes proof terms, and the kernel returns a verdict with counterexamples and iteration hints. Nobody is trusted; everybody is verified; authorship is recorded per discharged theorem.

Given a theorem whose proof term proves the wrong fact (the soundness gate rejects a term that establishes a different equality — proving something is not proving your claim):

$ allegro obligations pending.alg --pending
Obligation: theorem `double_four`
  proposition: double(2) == 4
  hash:        0728a8d1
  prior attempts: 1

$ allegro propose pending.alg          # the human worker: a TODO with hints
**Last failure:**
- reason: proof term establishes a different equality
- counterexample: theorem claims `double(2) == 4` but the proof
  proves `987654321 == 987654321`
**Hints:**
- the `by` proof term establishes a different fact than the theorem
  claims — match the proposition exactly

$ allegro prove pending.alg            # the LLM worker: same loop, autonomous
✓ double_four — by proof_refl(double(2))   [attempts: 1]
  authorship: {prover: <model-id>, attemptsUsed: 1, role: "primary"}

The model's proposal has no privileged path — it goes through the same proof_check as a human's edit, and a wrong term gets the same refusal. A benchmark finding we state up front: on our 10-obligation corpus, partial evaluation alone discharges every closed proposition — the prover's measured work is supplying proof terms that satisfy the soundness gate, which is exactly the loop above (bench/README.md).

Runnable versions of everything above, each with a "break it" block and captured failure transcripts, live in demos/rung1/.

A provable DSL — units of measure

The claim that Allegro is a platform has a falsifiable shape: a narrow domain surface built as an extension should inherit the entire kernel — types, refinements, theorems, discharge tiers, the assumption ledger — and be exactly as serious as the general-purpose language. Here is the test: a units-of-measure physics DSL, ~200 lines of Allegro, zero host code (lib/units.alg). Dimensions are structural data; named dimensions (Velocity, Force, …) are ordinary refinements over one Quantity record — so dimensional soundness is checked by the same machinery as PositiveInt, and the literal syntax (3 m, 9.8 m/s^2) comes from a ~10-line grammar block in the library.

Click Run to evaluate

Passing a length where acceleration is expected halts the build — a refinement check failure at the call site, the same "build safety in" path as every other refinement. And allegro verify renders the DSL's whole epistemic state in domain vocabulary — PE-discharged physics facts, the admitted transitivity with its backers, and the algebraic laws honestly pending (record-domain quantifiers await sample construction; the verdict says so instead of rounding up):

Verdict (verified): 6/6 discharged
  ✓ km_scale — by auto-PE
  ✓ newton_ident — by auto-PE
  ✓ f_ma — by auto-PE
  ✓ q_chain — by auto-PE [resting on admitted 'trans' of 'Quantity']
  laws: 12/17 discharged, 1 ADMITTED (assumed, not proof), 4 pending
    ! Quantity.trans (admitted)
    ? Quantity.mul_comm
    ? Quantity.conv_roundtrip
  assumption ledger: rests on 1 admitted, 0 sampled; 4 obligation(s) pending
    ! admitted 'trans' of 'Quantity' — backs: q_chain, p

What was written for physics: the dimension vectors, the unit table, the error messages. What was inherited free: the type checker, refinement discharge, the theorem machinery, the strict gate, the tier system, the ledger, the effects calculus, and the prover loop. Runnable scenes with break-it transcripts live in demos/rung2/.

Basics

Bindings, arithmetic, functions, and control flow. Allegro uses => for function definitions and if/then/else for conditionals.

Click Run to evaluate

Types

Every value in Allegro Standard has a type. Types enable dot-access dispatch, type checking, and compile-time inference. Built-in types include Int, Float, String, Bool, Array, and Object.

Click Run to evaluate

Pattern Matching

Pattern matching with when/is/then. Supports literals, wildcards, bindings, type destructuring, structural destructuring, nested patterns, and guard clauses.

Click Run to evaluate

Collections

Arrays support bracket access, map, filter, reduce, and chaining. Objects support dot access and destructuring.

Click Run to evaluate

Custom Types

Create types using the fluent API. extend creates record types, distinct creates newtypes. Types themselves are typed values — Int instanceof Type is true.

Click Run to evaluate

Interfaces

Interfaces declare required members using structural type matching. Any type with the right members satisfies the interface — no implements keyword needed.

Click Run to evaluate

Mixins

Method implementations are ordinary define spec entries — an entry whose value is a function becomes a method receiving self as its first argument. Reusable mixins are methods-only types (bundles) drawn alongside other bundles.

Click Run to evaluate

Error Handling

Errors are values, not exceptions. They propagate automatically through operations. Use error of to inspect, and pattern matching to handle.

Click Run to evaluate

Implicit Async

Allegro handles async operations without await. Expressions that depend on unresolved futures automatically defer and re-evaluate when results arrive. print streams output as values become available.

Click Run to evaluate

Grammar Extensions

Allegro exposes its Earley parser as first-class primitives. Build a grammar at runtime, parse strings into trees of Allegro values, and interpret those trees in pure Allegro — build a DSL in a page of code.

The example below builds a minimal regex DSL: literal chars, | alternation, */+/? postfix. The grammar is defined with grammar_terminal, grammar_phrase, grammar_choice, grammar_repeat, grammar_optional. The parse tree is then interpreted by pure Allegro functions to produce a matcher.

// Build a regex DSL grammar — literals, |, *, +, ?, ( )
g = grammar_new({whitespace: ""})
chr  = grammar_terminal(g, "/[a-z]/")
pipe = grammar_terminal(g, "|")
lp   = grammar_terminal(g, "(")
rp   = grammar_terminal(g, ")")

// Recursion hook: forward-declare pattern, bind later
pattern = grammar_choice(g, [])
grouped = grammar_phrase(g, [lp, pattern, rp])
base    = grammar_choice(g, [chr, grouped])
postfix = grammar_choice(g, [
  grammar_terminal(g, "*"),
  grammar_terminal(g, "+"),
  grammar_terminal(g, "?")])
atom    = grammar_phrase(g, [base, grammar_optional(g, postfix)])
concat_rule = grammar_repeat(g, atom, {min: 1})
alt_rule    = grammar_repeat(g, concat_rule, {min: 1, delimiter: pipe})
grammar_choice_add(pattern, alt_rule)
grammar_set_target(g, pattern)

// Interpret the parse tree as a matcher (pure Allegro)
match_base(n, s) =>
  if n instanceof String then
    if s.length > 0 && s.charAt(0) == n then s.slice(1, s.length) else none
  else match_pattern(n[1], s)

match_atom(a, s) =>
  when a[1]
    is none then match_base(a[0], s)
    is "*" then match_star(a[0], s)
    is "+" then match_plus(a[0], s)
    is "?" then match_opt(a[0], s)

match_star(n, s) => when match_base(n, s) is none then s is r then match_star(n, r)
match_plus(n, s) => when match_base(n, s) is none then none is r then match_star(n, r)
match_opt(n, s)  => when match_base(n, s) is none then s is r then r

concat_from(a, i, s) =>
  if i >= a.length
    then s
    else when match_atom(a[i], s)
      is none then none
      is r then concat_from(a, i + 1, r)

match_concat(a, s) => concat_from(a, 0, s)

pattern_from(c, i, s) =>
  if i >= c.length
    then none
    else when match_concat(c[i], s)
      is none then pattern_from(c, i + 1, s)
      is r then r

match_pattern(c, s) => pattern_from(c, 0, s)

matches(pat, str) =>
  when match_pattern(grammar_parse(g, pat), str)
    is none then false
    is r then r.length == 0

print(matches("(ab)+", "abab"))   // true
print(matches("a|b|c", "b"))      // true
print(matches("a*b", "aaab"))     // true
print(matches("a?b", "aab"))      // false

Click Run to evaluate

Runtime Grammar

Beyond building standalone DSL grammars, Allegro lets modules extend the host language itself. Inside a grammar { … } block, a module declares new operators, keywords, or entire multi-token expressions. Files that opt in with a use NAME header get those syntactic additions before parsing starts.

Four operator-level declarations plus user rules and multi-token forms, all sharing one grammar block:

infix S prec(X) left/right/none => (l, r) => ast — binary operator at a named precedence level
prefix S at(X) => x => ast — unary prefix symbol (e.g. #x)
postfix S at(X) => x => ast — unary postfix symbol (e.g. n!)
expr_prefix KW => x => ast — keyword followed by one expression (e.g. neg x)
rule NAME = ebnf => template — user sub-rule used by forms
expr_form parts => template — multi-token inline expression (match x with …)
stmt_form parts => template — multi-token statement form

Precedence is named, not numeric. Use at(mul) to place at an existing level, prec(pow) above(mul) below(unary) to declare a new level between existing ones, or at("*") to look up by operator symbol.

Here's lib/pow.alg — adds ** and neg:

pow_helper(base, n, acc) =>
  if n == 0 then acc else pow_helper(base, n - 1, acc * base)

pow_int(base, n) => pow_helper(base, n, 1)

pow_grammar = grammar {
  infix "**" prec(pow) above(mul) below(unary) right => (l, r) => pow_int(l, r)
  expr_prefix "neg" => x => 0 - x
}

A consumer file declares use pow at the top and uses the new syntax as if it were built in:

Click Run to evaluate

Multi-token forms let a single module ship a whole new expression shape. Here's lib/match_expr.alg — a match x with p => e | … form that desugars to a linear search:

match_helper(scrutinee, cases, idx) =>
  if idx == cases.length
    then error "match: no branch matched"
    else if scrutinee == cases[idx].p
      then cases[idx].e
      else match_helper(scrutinee, cases, idx + 1)

match_dispatch(scrutinee, cases) =>
  match_helper(scrutinee, cases, 0)

match_grammar = grammar {
  rule match_case = p:expr "=>" e:expr      => (p, e) => {p: p, e: e}
  rule match_list = c:match_case ** "|"      => c => c

  expr_form "match" s:expr "with" cs:match_list
    => (s, cs) => match_dispatch(s, cs)
}

EBNF inside a rule body: "literal", ident references, s:rule labels, a* / a+ / a? repetition, a ** sep separator-rep, (a | b) alternation. Templates receive labels as positional params.

Click Run to evaluate

The mechanism is module-scoped — only files that use-declare pow or match_expr see those additions. Cross-module conflicts (two modules registering the same operator, cyclic precedence declarations) surface at use time with aggregated error messages. Other files still parse as plain Allegro Standard.

More forms (Phase 7)

A few more ways to declare and activate grammars:

new grammar { … } — fresh grammar, not an extension of Allegro. Used for standalone DSLs.
grammar extends X { … } — build on any existing Grammar value, not just Allegro.
use grammar { … } — declare a grammar inline at the top of a file, no separate module required.
use NAME.MEMBER — select one specific Grammar binding from a module that exports several.
rule foo += body => template — append an alternative to an existing production.
rule foo[alt] = body => template — replace a single named alternative.
rule foo -= alt — remove an alternative.

Templates are hygienically substituted: symbols inside a grammar block resolve against the module that declared the block, not the consumer's scope. A consumer that happens to rebind a name the template uses can't silently hijack the grammar extension.

Click Run to evaluate

Recursive Algorithms

Allegro supports tail call optimization. Write recursive algorithms naturally — they use O(1) stack space when in tail position.

Click Run to evaluate

Want to explore more?

Open the Full Sandbox

Allegro

Provability — the headline example

Refinement types & domain propagation

Asserts

Lifecycle invariants

Contracts: requires & ensures

Effects — the negative aspect

Laws — every claim carries its strength

The prover loop — one protocol, any participant

A provable DSL — units of measure

Basics

Types

Pattern Matching

Collections

Custom Types

Interfaces

Mixins

Error Handling

Implicit Async

Grammar Extensions

Runtime Grammar

More forms (Phase 7)

Recursive Algorithms

Contracts: `requires` & `ensures`