Bend是一款基於以下前提建立的編程語言：隨著AI代理越來越多地生成軟件，人類需要一種方法來驗證生成的代碼是否正確實現了他們的意圖。該語言引入了一種機制，開發者可以宣告「法則」——即應用程序絕不可違反的精確且無歧義的規則。例如，開發者可能會宣告一條法則，規定特定的遊戲狀態是無法達到的。當AI代理嘗試修改代碼時，Bend編譯器充當守門人：除非AI能同時提供數學證明來證明新代碼符合這些法則，否則它將阻止任何違反這些法則的合併操作。
此視覺效果說明了宣告「法則」以防止不可能的遊戲狀態的概念。
此圖像展示了Bend編譯器的「法則」旨在防止的錯誤類型。
此視覺效果展示了成功執行數學法則以維護遊戲完整性的情況。
Bend的技術核心是其編譯器，它作為一個高速證明檢查器運行。雖然像Lean或Rocq這樣的傳統證明助手可能需要數分鐘來驗證中型代碼庫，但Bend旨在在一秒內完成這些檢查。這種速度允許AI代理在每次增量變更後驗證正確性。此外，Bend旨在提供高性能，編譯為在單個CPU核心上運行速度幾乎與C語言一樣快的原生代碼。它還支持大規模並行處理，允許代碼在數千個GPU核心上運行，而無需手動管理線程或編寫內核，因為該語言會自動處理工作分配。
此圖表支持了Bend在不到一秒內執行檢查的聲明，遠快於傳統工具。
此圖表說明了Bend幾乎能與C一樣快以及支持大規模GPU並行的能力。
此動畫展示了該語言在無需手動管理線程的情況下處理大規模並行的能力。
儘管Bend承諾提供「無錯誤」的代碼，但使用它涉及特定的權衡和實際障礙。由於該語言需要形式化證明，甚至基礎算術運算也可能要求開發者或AI定義基礎屬性。例如，有用戶報告稱，由於基礎庫缺乏完整的序理論，AI代理在處理某些算術法則時遇到了困難，需要AI為最大值等基本函數編寫結構遞歸證明。此外，雖然Bend為驗證意圖提供了強大的框架，但為高度複雜的系統定義這些「法則」的複雜性，仍是那些從自然語言規範轉向的開發者需要考慮的重要因素。該項目目前處於早期階段，且缺乏公開的提交歷史已被指出作為評估其長期開發和可靠性的考慮點。