Bend is a new programming language designed for a post-AGI economy, focusing on high-performance execution and verifiable correctness through formal proofs. Built on affine dependent type theory, the language utilizes strong types, purity, and linearity to achieve performance comparable to hand-written C on CPUs and CUDA on GPUs. Its architecture supports full memory unification and massive parallelism, allowing tasks to be distributed across thousands of GPU cores without the need for manual thread management or locks. A core feature is the "LAWS.bend" system, which allows developers to define mathematical invariants—such as ensuring a game state remains unwinnable or a list remains sorted—that the compiler must verify via "PROOF.bend" files. This mechanism ensures that AI-generated code adheres to specified constraints by demanding formal proofs whenever the codebase is modified. While the language currently lacks features like type classes or automated proof search, it targets C, Metal, CUDA, and JavaScript, offering a high-speed alternative to traditional proof assistants by performing verification in seconds rather than minutes.