How to Build and Verify Agent-Written Code with Bend 2

Superlinear · Oct 2, 2026 · 52m · transcript

Bend2 puts code and proofs in the same language, so coding agents can write both. Tests check examples. A checked proof can establish that a specific rule holds for every allowed input.

This is formal verification, an additional verification layer alongside types and tests. You still need to review whether the rule captures the behavior you actually want.

In this episode, we show how to choose rules worth proving, get the agent to finish the proofs, and decide where the extra effort pays off. We uncover false proposed rules and integrate a Bend core with checked editing rules into an existing…