Just like Cursor reimagined the code editor for the AI era, Bend2 reimagines the language itself. It integrates AI-driven generation, verification, and synthesis, solving a critical limitation of current LLM workflows: the AI Doom Loop — where projects stall as AI-generated codebases grow and accumulate subtle bugs. With Bend2, every generated function is required to pass rigorous tests or even full proofs, enforced at compile time. This keeps correctness local and avoids error accumulation, letting users build much larger codebases using AI.

The key enabler behind this is our proprietary technology: NeoGen, a symbolic synthesizer that finds recursive functions from specs (tests or theorems) up to 10,000x faster than existing tools like Myth. When the user types gen, NeoGen tries to synthesize a function first. If it fails, an LLM is called — but always under the discipline of formal correctness. This makes AI code generation in Bend2 not just faster, but safer and more scalable.

Bend2’s syntax is Pythonic, with a Haskell-inspired type system, and includes first-class support for dependent types and theorem proving. It compiles to HVM, our ultra-fast runtime that runs symbolic code on the GPU. While the language will be 99% open-source and work offline for free, generative features (like gen) will be metered through a paid API — providing our business model.

We’re raising $4M at a $60M valuation to bring Bend2 to market. Funds will be used to complete the language, integrate LLMs, build dev tools (LSP, editor, docs), and grow adoption. We believe Bend2 can unlock a new class of applications — complex, large-scale software written entirely by AIs, with correctness guarantees built-in. Join us in building the foundation for AI-native programming.

Here is a full informal spec (yes, this is a ChatGPT link - ask it questions!)

About Us

We're the team behind:

- HVM: the world's fastest λ-Calculator (a "β-optimal" function compiler).

- Bend: the first GPU-native language featuring unrestricted recursion.

- Kind: a modern functional programming language and proof assistant.

---

Note: due to NeoGen's success in internal benchmarks, we've updated the immediate goals to turn it into a product, as a paid feature inside Bend2. Our aim is to continue program synthesis research (towards a symbolic transformer) in 2026. Here's our previous pitch.