ALIVE

An AI-native formally verified programming language.

ALIVE is designed under the premise that AI is the primary producer of code, and the compiler's role is verification, not assistance. Every compiler error is a structured JSON object — not a text string — that an AI agent can mechanically interpret and repair.

-- Proof-carrying code: verified increment
module Verified

spec increment(x: Nat) -> Nat {
    ensures true;
    succ x
}

---

Design Invariants

Invariant	Meaning
I1	Every function carries a machine-checkable proof of correctness
I2	All compiler errors are structured JSON objects
I3	Complete formal semantics — no undefined behavior
I4	Effects are first-class and tracked in the type system
I5	The language is self-describing: its semantics are expressible within it

---

Three-Layer Architecture

SPEC  — WHAT must be true    (pre/post conditions, invariants)
IMPL  — HOW to compute       (executable terms)
PROOF — WHY impl satisfies spec (proof terms, verified by the compiler)

The compiler checks PROOF against SPEC. On failure, it emits a VerificationFailure — structured data an AI agent uses to mechanically repair the proof.

---

Features

• Bidirectional type checking — inference (Γ ⊢ t ⇒ A) and checking (Γ ⊢ t ⇐ A) disciplines
• Dependent types — Π-types, Σ-types, propositional equality Eq(A, a, b)
• Universe hierarchy — Type[0], Type[1], ... (no Type-in-Type)
• Proof system — Fourier-Motzkin elimination for QF_LIA, Z3 SMT backend, CEGIS loop invariant synthesis
• Effect tracking — Pure, State, IO, Prob, Ndet
• Rust backend — transpiles ALIVE to Rust; linear types map to ownership/move semantics
• Python backend — transpiles ALIVE to Python
• Formal translation validation — model-theoretic + bounded exhaustive checking that the Rust/Python output matches ALIVE semantics
• Concentration bounds — Markov, Chebyshev, Chernoff, Hoeffding inequalities as proof primitives

---

Structured Errors for AI Consumption

When a postcondition fails, the compiler produces:

{
  "type": "VerificationFailure",
  "vc_id": "post_0",
  "vc_expression": "result >= x + y",
  "counterexample": {"x": 1, "y": 2, "result": 2},
  "suggestions": [
    {
      "type": "StrengthenPrecondition",
      "function": "add",
      "condition": "y = 0",
      "reason": "Current implementation only works when second argument is zero"
    }
  ]
}

An AI agent receives this and mechanically selects and applies the repair — no natural language parsing required.

---

Syntax

-- Identity and constant functions
module Hello

fn identity(x: Nat) -> Nat {
    x
}

fn const_three(x: Nat) -> Nat {
    let three = succ (succ (succ zero));
    three
}

-- Arithmetic with specifications
module Arithmetic

fn add(x: Nat, y: Nat) -> Nat {
    x
}

spec add_commutative(x: Nat, y: Nat) -> Nat {
    requires true;
    ensures true;
    x
}

---

Quickstart

git clone https://github.com/qosu/alive.git
cd alive
pip install -r requirements.txt   # z3-solver
python3 -m pytest tests/ -q       # 156 tests

Run the full pipeline demo:

python3 examples/demo.py

---

Project Structure

src/
  ast.py                  — AST nodes: Π, Σ, Eq, effects, proof terms, holes
  parser.py               — Lexer + recursive descent parser
  typecheck.py            — Bidirectional type checker (inference + checking)
  elaborator.py           — Elaboration pass (holes, implicit arguments)
  eval.py                 — Call-by-value evaluator (substitution, reduction)
  proof.py                — Fourier-Motzkin + DPLL(T) for QF_LIA
  z3_backend.py           — Z3 SMT interface
  cegis.py                — CEGIS loop invariant synthesis
  smt_engine.py           — SMT engine abstraction layer
  verifier.py             — Verification condition generator
  rust_backend.py         — ALIVE → Rust transpiler
  transpiler.py           — ALIVE → Python transpiler
  formal_translation.py   — Translation correctness framework
  translation_validator.py — Model-theoretic + bounded exhaustive validation
  covariance_check.py     — Covariance analysis
  concentration.py        — Concentration bound inequalities
  miller.py               — Miller's algorithm
  errors.py               — Structured error types (AliveError hierarchy)
tests/
  test_kernel.py          — 156 tests: AST, parser, type checker, evaluator, proofs
examples/
  hello.alive             — Identity and constant functions
  arithmetic.alive        — Arithmetic with specifications
  proof.alive             — Proof-carrying code
  demo.py                 — Full pipeline demonstration (parse → typecheck → eval → proof)
ALIVE.md                  — Formal language specification (BNF, typing rules, semantics)

---

Formal Specification

ALIVE.md contains the complete formal specification:

• Abstract syntax (BNF grammar)
• Operational semantics (call-by-value reduction rules t ⇓ v)
• Bidirectional type system (all inference and checking judgments)
• Proof system and verification condition generation
• Structured error format (AliveError, VerificationFailure, Suggestion)

---

Meta-theoretic Properties

• Type Safety — well-typed terms reduce to well-typed values
• Normalization — every well-typed term in the pure fragment reduces to a value
• Decidability — type checking is decidable for the kernel (no first-class dependent pattern matching)
• Consistency — no closed proof of Eq(Nat, zero, succ zero)

---

Bootstrap Path

• Phase 1 (current) — Python kernel: parser, type checker, evaluator, proof checker for QF_LIA
• Phase 2 — Self-hosting: ALIVE compiler written in ALIVE, compiled by the Phase 1 kernel
• Phase 3 — Verified self-hosting: formal proof that the ALIVE compiler correctly implements this specification

---

License

MIT