» Etiket
formal-verification
13 yayınMaith: Yapay Zeka Destekli Matematik Araştırması İçin Disiplinli Çerçeve
Maith, Riemann ve P vs NP gibi açık matematik problemlerini yapay zekayla araştırırken katı ispat standartları uygulayan açık kaynaklı bir çalışma alanı.
AI COBOL'u Java'ya Hızla Taşır, Doğruluğunu Kanıtlamak Asıl Zorluk
AI, COBOL'u Java'ya hızla taşıyor ama doğruluğu kanıtlamak farklı bir sorun. SMT tabanlı eşdeğerlik doğrulayıcının gizli hataları nasıl yakaladığını görün.
Kani: Rust için model checker doğrulama aracı
Kani, Rust'ın MIR temsilini CBMC doğrulama motoruna aktararak unsafe kod, fonksiyonel doğruluk ve panic içermemeyi kanıtlıyor; Rust standart kütüphanesinde binlerce harness ile üretimde çalışıyor.
CommitBrief — terminalde yapay zekâ destekli kod incelemesi
Staged değişiklikleri, bir commit aralığını ya da bütün bir GitHub pull request'ini yerelde inceleyen sağlayıcı bağımsız CLI. Sıfır telemetri, sunucu yok. Açık kaynak, GPL-3.0.
commitbrief.comLLM Destekli Formal Doğrulama nftables'ta İki Kritik Hata Buldu
Basis, LLM destekli formal doğrulama ile Linux'un nftables optimizasyoncusunda 2022'den beri süregelen iki kritik hata keşfetti.
Provensql: İki SQL Sorgusunun Eşdeğerliğini Matematiksel Olarak Kanıtlıyor
Provensql, SQL sorgularının eşdeğerliğini SMT tabanlı kanıtlarla doğrulayan açık kaynak araç; LLM yargıçlardan farklı olarak asla yanlış pozitif vermez.
Formel Doğrulamalı 3D CSG: 1000 Satır AI Kodu Değil, 93 Satır Spec'e Güvenin
Lean 4'te formel doğrulanmış 3D mesh kesişim çekirdeği: 93 satır spec, 60.000+ satır AI-üretimi kanıt, sıfır LLM güveni.
GDSII'den Devreye: Jane Street'in Yonga Bulmacasını Tersine Mühendislik
Jane Street bulmacasının ham GDSII yonga düzeni, 722 kapılık doğrulanmış bir Verilog netliste dönüştürülerek 11x11 Star Battle çözüldü.
Agent Control Plane: LLM Önerir, Yetkilendirme Asla Modelde Değil
ACP mimarisi, AI ajanlarında LLM'in önerdiği eylemleri prompt injection'a kapalı bir politika motorunda yetkilendiriyor; kanıtlanabilir ve test edilebilir.
Otonom AI Ajanları için Çekirdek Seviyesinde Denetim: eBPF-LSM + Z3
eBPF-LSM ve Z3 SMT ile AI ajanlarını çekirdek seviyesinde denetleyen açık kaynak prototip; ölçülen performans, sınırlamalar ve break-it challenge.
Arduino için Donanım Modeli PLC Doğrulamasındaki Yanlış Alarmları Gideriyor
Arduino tabanlı endüstriyel kontrol sistemlerinde IEC 61131-3 PLC kodu için donanım farkındalıklı doğrulama, yanlış alarmları ortadan kaldırıyor.