yapay zeka modellerinin ürettiği kod ve mantık hatalarını, çalışma zamanında ispat (proof) mekanizmasıyla engelleyen yeni bir programlama dili. geleneksel yaklaşımdan farkı, hataları test aşamasında yakalamaya çalışmak yerine tip sistemi ve matematiksel ispatlarla derleme anında dışlaması; üstelik bunu hem cpu hem gpu üzerinde paralel çalışacak şekilde tasarlaması.
llm destekli kod üretiminin patladığı şu dönemde en büyük sorun, modelin kendinden emin bir şekilde yanlış kod yazması. bend burada devreye giriyor: üretilen kodun doğruluğunu ispat zorunluluğuna bağlayarak halüsinasyon kaynaklı hataların üretim hattına sızmasını yapısal olarak engelliyor. rust'ın bellek güvenliği yaklaşımına benzer bir felsefe ama kapsamı daha geniş; sadece bellek değil, iş mantığının doğruluğunu da ispat istiyor. cpu-gpu birleşik çalışma modeli ise onu bilimsel hesaplama ve yapay zeka eğitim boru hatları için cazip kılıyor. dezavantajı, ispat yazmanın öğrenme eğrisinin dik olması ve mevcut kütüphane ekosisteminin henüz olgunlaşmamış olması. yine de ai çağında "önce doğrula sonra çalıştır" paradigmasının ana akıma taşınması açısından dikkate değer bir adım.