» Tag
formal-verification
10 postsMaith: A Disciplined Framework for AI-Assisted Math Research
Maith is an open-source workspace enforcing rigorous proof standards when using AI to explore unsolved math problems like Riemann and P vs NP.
AI Migrates COBOL to Java Fast — Proving It's Correct Is Hard
AI speeds up COBOL-to-Java migration, but proving correctness is the hard part. How an SMT-based equivalence verifier catches hidden bugs before they ship.
Kani: A Model Checker for Rust Verification
Kani compiles Rust's MIR into CBMC's engine to prove unsafe-code soundness, functional correctness and panic-freedom, running thousands of harnesses in production CI for the Rust standard library.
CommitBrief — AI code reviews, right in your terminal
A provider-agnostic, local-first CLI that reviews your staged changes, a historic range, or a whole GitHub pull request. Zero telemetry, no server. Free and open source.
commitbrief.comLLM-Assisted Formal Verification Uncovers Two Critical nftables Bugs
Basis used LLM-guided formal verification in Rocq to audit Linux's nftables optimizer, uncovering two critical bugs since 2022.
Formally Verified 3D CSG: Trust a 93-Line Spec, Not 1000 Lines of AI Code
First formally verified 3D mesh intersection kernel in Lean 4: a 93-line spec replaces review of 1000+ lines of AI code and 60,000+ lines of proofs.
Agent Control Plane: The LLM Proposes, It Never Authorizes
Agent Control Plane keeps AI agent authorization outside the model, blocking prompt injection with signed policy and human sign-off for risky actions.
Kernel-Level Enforcement for AI Agents via eBPF-LSM and Z3
Solo-built eBPF-LSM prototype enforces AI agent guardrails at the kernel syscall boundary with Z3 SMT checks; open break-it challenge on GitHub.
Hardware-Aware Model Fixes False Alarms in PLC Verification for Arduino
A hardware-aware verification method eliminates false alarms in formal analysis of IEC 61131-3 PLC code deployed on Arduino-based industrial controllers.
Alerus Brings Formal Verification to Probabilistic Rust Code
Alerus extends Verus with error-credit reasoning to formally verify randomized sampling algorithms in real Rust code, with soundness proved in Rocq.
The Lean Theorem Prover: Design and Evolution Overview
Lean plays a crucial role in formal verification and AI integration. Lean FRO was established in 2023.