Bend2 for verified parallel agents

Bend2 for verified parallel agents

One-liner

Bend2 (bendlang/bend) = affine dependent types + human-owned LAWS.bend + AI-owned PROOF.bend + BendRT CPU/GPU — framed as “AGENTS.md backed by proof.” Young stack: no tactics, AI-written compiler, checker↔Lean formalization mismatches. Use for greenfield parallel+laws; prefer Lean/Dafny/Verus/TLA for library-heavy or mature CI.

Related: 2026-09-27 Formal verification in agent-driven development · 2026-09-27 Lean 4 agents for verified software · 2026-09-27 Agent FV toolbox and DIY playbook · Cloud agent orchestrator

---

Confidence

Claim	Confidence	Note
Bend2 is a real public Apache-2.0 language with laws/proofs + BendRT	High	bendlang/bend README + GUIDE
Bend2 = Bend1 / HVM2	False	Explicit: “Bend 1 programs and HVM do not carry over”
Production-ready metatheory-certified compiler	Low	Compiler ~99% AI-written / unaudited; checker unproven except --safe; documented Lean formalization mismatches (what-is-bend2)
Checker speed ⇒ better agent proof economics	Low	Check 0.295s vs Lean 36s on synthetic 12.8k defs — not mathlib port; missing tactics can raise LLM repair cost (bend2-vs-lean)

---

1. Bend2 vs Bend1 (disambiguation)

Artifact	Org / repo	Runtime	Proof story	Parallelism
Bend 1	HigherOrderCO/Bend	HVM2	No dependent law language in published Bend1 syntax	Automatic parallel reduction; run-cu CUDA
Bend 2	bendlang/bend · bend-lang.com	BendRT (C; Metal/CUDA via f!)	Dependent types + law / proof def; LAWS.bend + PROOF.bend	Explicit balanced fork/join a b = f(x) g(y); no work stealing

Bend2 = Bend version 2, not a separate product name. Do not conflate when choosing a fleet stack (README extract).

Status pin in independent notes: Bend 2.0.5 / limits as of 2026-09-20 (what-is-bend2).

---

2. Laws / proofs / agent workflow

Upstream framing: ambiguity-free intents for AI builders — laws more precise than NL, proofs that edits obey them, fast CPU/GPU execution.

LAWS.bend    # human claims (AI must not edit)
PROOF.bend   # AI proofs: def Laws.<name> mirrors law <name>
bend PROOF.bend           # CI gate — "All terms check."
bend PROOF.bend --safe    # + BendTT Lean kernel recheck

From GUIDE / README

“In short, LAWS.bend is AGENTS.md backed by proof.” · “Bend has no tactics or proof search; proving theorems takes extra effort.”

Proof dialect (canonical tutorial)

From bend2.dev/learn/proofs (half_ok worked example):

1. Predicate as type (IsEven(n): Type via match; odds → Empty).
2. Executable half by structural match.
3. law half_ok with for x: Nat / for e: IsEven(x) / {Nat.double(half(x)) == x : Nat}.
4. def half_ok proves the law: {==} when sides compute equal; Empty elim via empty match; recursive IH with rewrite motive %ih : motive where _ marks the replaced slot.
5. Recursion must use structurally smaller arguments; @unsafe bypasses and leaves proof discipline.

Agent repair target: emit matching law+def, use {==}, %ih : motive, Empty-elim — no tactics to lean on (learn/proofs extract).

Parallelism + effects

• Fork/join: programmer splits; fixed assignment, no work stealing — uneven trees are the author’s problem.
• f!(x) marks GPU (Metal/CUDA); IO stays on host.
• Affine ownership independent of app laws: plain Array<T> one owner; + / is Data for reuse.
• Numbers: Nat, U32, F32 only (no U64/I64/F64; Metal has no f64). F32 axiomatic — nothing about FP can be proven.
• Effects (print, env, files, TCP/UDP, …): foreign C/JS outside source proofs. “A source-level proof over Order does not verify that foreign implementation, the database… or the network.” (what-is-bend2)

Upstream M4 Max pins (Bend modes only): Game of Life 7.803s → 0.647s parallel CPU → 0.063s GPU; Lexer 2.144s → 0.198s / 1.075s GPU.

---

3. Bend2 vs Lean (fleet design)

Dimension	Lean 4	Bend 2
Proof construction	Terms or tactics; huge automation	Explicit proof terms; no tactics (2.0.5 notes)
Proof reuse	mathlib + packages	Base + demos; small
Native parallel	Tasks / RC	Balanced fork/join
GPU	Foreign / external	Marked ! on Metal/CUDA
Agent maturity	Many harnesses + benches (Vero, CLEVER, …)	Young; community reports agent proof effort can be harder than Lean for same claim (seed cites yalexey)
Trust story	Mature kernel + public compiler	Checker/compiler evolving; --safe → BendTT Lean kernel (bendtt.lean, Lean v4.34.0)
Checker synth bench (M4 Max, 12.8k defs)	36.177 s	0.295 s

Choose on product shape, not checker OOM claims

“Bend suits an evaluation where affine code and native CPU/GPU execution are requirements and the project can supply its own proofs. Lean supplies existing mathematical libraries and tactics…” (bend2-vs-lean). Proof construction cost dominates agent loops.

Hybrid (engineering, not prescribed by notes): Lean for hard theory / audit of BendTT; Bend for shipping parallel app with LAWS gate — mismatch disclosure supports treating Bend checker as engineering trust, not drop-in Lean substitute.

---

4. Maturity caveats (must state)

From README + what-is-bend2:

1. Compiler ~99% AI-written, not fully audited.
2. Checker has no proof and may have bugs; --safe uses a proven kernel — but translation to .bendtt itself is unproven.
3. Mismatches between checker and its Lean formalization are documented.
4. “A correct source proof cannot compensate for a compiler bug that changes the program’s meaning.”
5. Young ergonomics: verbose (no inference), no typeclasses/traits/macros beyond templates, no if-then-else (match Bool), strings = char linked lists, one C file / no incremental builds, no Windows (WSL ok), no TLS/HTTP/JSON/regex yet, terse errors, no debugger/REPL/test framework beyond guide.
6. Weak laws are easy to “prove” and useless — same failure mode as every FV stack; Bend’s agent-facing UX makes overclaim more tempting.
7. Game demo LAWS/PROOF cover model properties (e.g. safe-position) — not unmentioned requirements, JS renderer, or compiler correctness.

Victor Taelin proof-economics framing (seed): “1 line of code, tens of lines of proof” — AI shifts cost calculus but doesn’t erase it (x.com/VictorTaelin/status/2102764825231470862).

---

5. When to use Bend2 in a fleet

Try Bend2 when

• Greenfield numerical / parallel backends where agents should own both speedups and a small set of invariants.
• Product is the parallel program (affine + fork/join + ! GPU).
• Team accepts explicit proofs + young tooling; can pin SHAs; can keep laws human-owned.
• CI can run bend PROOF.bend fail-closed; release gates prefer --safe + review .bendtt.

Prefer Lean / Dafny / Verus / TLA+ when

• Need mathlib/tactics, existing verified artifacts, or industry analyzers.
• Agent already strong on Lean harnesses (Vero-style).
• Domain needs FP64, HTTP/TLS stacks, Windows-native, or large library ecosystems.
• You need mature agent benches and repair literature.

DIY gate sketch (Herdr / Cloud agent orchestrator)

Human writes / reviews LAWS.bend
  → coding agent edits code + PROOF.bend
  → bend PROOF.bend  (fail → repair ≤ N)
  → bend PROOF.bend --safe  (release / merge)
  → measure runtime separately (CPU/GPU) — checker throughput ≠ program speed ≠ proof effort

Marketing vs guarantee

Laws only cover what you wrote. Foreign/IO/DB/network are outside the proof. Review law strength as part of the program — weakening a requirement makes its proof easier and its value lower.

---

Sources

• github.com/bendlang/bend · extract sources/bend-a-fast-language-that-blocks-ai-mistakes-via-proof.md
• What is Bend2? · sources/what-is-bend2.md
• Bend2 vs Lean · sources/bend2-vs-lean.md
• Learn proofs · sources/bend2-learn-proofs.md
• Bend1 ancestor — HigherOrderCO/Bend
• Seed — 2026-09-27 Formal verification in agent-driven development