Mandatory preconditions, postconditions, and entity invariants. Z3 SMT verification via intentc verify. Natural-language intent blocks that resolve to specific contract references. One source file compiles to Rust, JavaScript, and WebAssembly.
Camp: Verification
Author: lhaig
Implementation language: Go
Compilation target: Native binaries (via Rust), JavaScript, WebAssembly (direct binary)
Licence: Apache-2.0
First seen: February 2026
Maturity: working compiler
Agent tooling:
- AGENTS.md
- CLAUDE.md
- INTENT.md
Every function carries requires/ensures; every entity carries an invariant; loops carry invariant and decreases. An intent block links natural-language goals to specific contract references via verified_by, and the compiler refuses to resolve a reference that has no matching contract. intentc verify discharges what it can to Z3; what remains runs as enforced runtime checks in Rust (panic), JavaScript (throw), or WebAssembly (trap), all from the same source file.
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.
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.
requires/ensures; entities carry invariant; loops carry invariant/decreases. The grammar reserves the slots; the type checker enforces that verified_by references resolve.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.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.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.intentc test-gen derives property-based tests from requires/ensures, complementing — not replacing — the SMT discharge.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.
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.
<Inference> effect; Intent keeps names and concentrates its novelty in intent blocks that bind natural-language goals to verified contract references.verify blocks as Lean 4 theorems or Dafny lemmas through aver proof, lifting effectful code into proof artefacts via Oracle; Intent commits to Z3 SMT with runtime enforcement on every backend. Same diagnosis, different upper-bound check.Last modified 15 June 2026