Intent.

The thesis.

Intent’s premise is that humans audit contracts, not implementations. The repository’s framing makes the position explicit: “Humans audit contracts, not implementations. When you generate Intent code, the human reads your requires, ensures, invariant, and intent blocks to verify correctness.” The compiler enforces structural consistency between the natural-language declarations and the machine-checkable ones — every verified_by reference must resolve to an actual requires, ensures, or invariant clause, or the program fails to compile.

The contract system is the product. The implementation is secondary.

The distinctive move is the intent block itself: a named natural-language goal paired with a list of verified_by references that name specific contracts in the codebase (BankAccount.invariant, BankAccount.deposit.requires, BankAccount.withdraw.ensures). The compiler resolves each reference during semantic analysis and emits an error on a dangling one; published intent blocks therefore cannot drift from the contracts they cite. Z3 discharges what it can statically via intentc verify; the rest becomes runtime enforcement that fires identically across all three targets — a requires failure panics the Rust binary, throws an Error in JavaScript, and traps in WebAssembly.

What it looks like.

entity BankAccount {
    field balance: Int;

    invariant self.balance >= 0;

    method deposit(amount: Int) returns Void
        requires amount > 0
        ensures self.balance == old(self.balance) + amount
    {
        self.balance = self.balance + amount;
    }
}

intent "Safe withdrawal preserves non-negative balance" {
    goal "BankAccount.withdraw never results in balance < 0";
    guarantee "if withdraw returns false then balance is unchanged";
    verified_by BankAccount.invariant;
    verified_by BankAccount.withdraw.requires;
}

old(...) captures pre-mutation state for ensures clauses. forall i in 0..n: p and exists i in 0..n: p quantify over integer ranges in contracts. Loops carry invariant and decreases clauses for inductive reasoning at verification time.

Distinctive moves.

• Mandatory contracts at three levels. Functions carry requires/ensures; entities carry invariant; loops carry invariant/decreases. The grammar reserves the slots; the type checker enforces that verified_by references resolve.
• Intent blocks as compiled artefacts. A verified_by path (Entity.member.clause or function.clause) is resolved by the semantic checker, not by convention. Unresolved references are compile errors, which prevents prose-level drift between stated goals and machine-checkable contracts.
• Z3 as an optional static layer, runtime checks as the floor. intentc verify translates IR contracts to SMT-LIB and invokes Z3; results are reported per contract as verified / unverified / error / timeout. When Z3 is absent, the compiler degrades gracefully and the runtime asserts still run.
• Rust as IR, not as the only backend. An explicit IR layer (~30 node types, contracts as first-class IR nodes, OldCapture/OldRef as explicit pre-state) feeds three sibling backends: a Rust generator that hands off to cargo, a direct JavaScript emitter, and a direct WebAssembly binary emitter that does not require the Rust toolchain. Each enforces the same contracts at runtime.
• Property-based test generation from contracts. intentc test-gen derives property-based tests from requires/ensures, complementing — not replacing — the SMT discharge.

Maturity.

A Go workspace at v0.2.0 (released 16 February 2026) with 45 commits and 5 stars at time of cataloguing. The roadmap (docs/ROADMAP.md) records milestones 1–6 as complete: usable language surface (loops, arrays, enums, pattern matching, Result/Option, try operator, multi-file imports), the Z3 verifier (internal/verify/), and three working backends (Rust via internal/rustbe/, JavaScript via internal/jsbe/, direct WASM via internal/wasmbe/). The docs/DESIGN.md specification runs to 1,764 lines and notes that traits, generics, async/await, and a package manager with semver constraints have all landed since the POC. The CLI surface — intentc build / check / verify / fmt / lint / test-gen, plus intentc pkg init / add / remove / install — is shippable; a four-target showcase (CLI binary, browser dashboard, Node server, browser WASM at 155 bytes) runs against unmodified compiler output. Last commit was 25 March 2026; an LSP, REPL, and release-mode contract stripping sit on the milestone-8 roadmap and are not yet built.

Agent tooling.

Three documents target agent authors directly. AGENTS.md (~18 KB) is the Codex/general-agent orientation. CLAUDE.md is the Claude-specific working guide. INTENT.md (~26 KB) is the language reference written as agent instructions — it opens “You are generating code in Intent” and ends with ten explicit guidelines for AI code generation, including “Write contracts first” and “Every function should have contracts.” docs/REPRODUCE.md documents reproducing the compiler with the agent of the reader’s choice. Diagnostics are textual rather than structured JSON; the LSP that would expose them programmatically is on the roadmap rather than shipped.