AI Briefing#formal-verification
The latest AI and developer news about #formal-verification, with the original source and a short summary.
The latest AI and developer news about #formal-verification, with the original source and a short summary.
The system uses Gemini 4 models to solve open mathematical problems, rewrite C++ code in Rust, and optimize TPU kernels with verified results.
The 30-hour proof used about a third of the action tokens and was roughly 7x shorter than the 11-day September run.
The multi-LLM agentic framework generated over six million lines of Lean code to mathematically prove the security of the actual Signal code in four weeks.
A research prototype from Microsoft Research and GitHub Next that shifts review from line-by-line code to plain-language intent, using formal proofs to ensure agent-written Rust code matches specifications.
The report details the production of machine-checked proofs for 239 entry points across 123 libraries, identifying bugs that survived extensive fuzzing.
The 16 million-line library is the largest integrated formalized mathematics collection, enabling direct import of algebraic geometry definitions and theorems.
The algorithm, discovered by an internal research Claude model, solves #3-SAT in 2^(O(n log log n / sqrt(log n))) time and is formalized in Lean 4.
The 24-day formalization generated 43.1 million lines of code and identified 34 significant discrepancies in existing mathematical proofs.
The study demonstrates that AI can produce formal proofs for software properties, a distinct capability from code generation that helps identify defects missed by conventional testing.
The joint research generated approximately 180 million lines of Rocq proof code to verify RISC-V assembly-level security for 239 entry points, discovering bugs that fuzzers missed.
Researchers proved the 1995 Kannan-Lovász-Simonovits conjecture, establishing a dimension-free geometric principle for log-concave distributions.
Maxwell, a Code Execution Model by doubleAI available in early access, rewrites binaries at runtime with formal proof of semantic equivalence, achieving 1.86x speedups in LTX-2.5 video generation.
Basis Research used LLMs to write formal semantics for an extended WHILE language and prove in Lean that its compiled C interpreter's RISC-V binary execution matches those semantics.
Tao argues that AI's ability to mechanically verify and generate proofs requires decentering problem-solving to preserve human understanding and long-term mathematical health.
Experts highlight critical unresolved type-theoretic foundations and recent soundness bugs in Lean, even as AI tools like Anthropic and OpenAI accelerate large-scale mathematical formalization.
The withdrawal stems from a sign error in a stabilization-trace cancellation argument that invalidated dependent constructions in two other papers.
Researchers argue that semantic ambiguities in natural language make faithful AI autoformalisation computationally harder than the Halting problem, undermining confidence in the verification of OpenAI's claimed Navier-Stokes blow-up proof.
The proof was posted in a pinned GitHub commit on August 28, coinciding with a Fields Medalist's essay predicting AI would solve the problem before humans.
The pipeline generated over 3,000 machine-checked safety and liveness proofs from real-world TLA+ specifications using an agentic prover-reviewer loop.
Bend 2, a proof-oriented language designed to fail compilation when AI-generated code violates human-specified rules (LAWS.bend), has been released.
Analysis of major hash function collisions using AI tools confirmed that there is no tradeoff between hash speed and collision resistance.
AI agents generated an LSP server, decompiler, and 95 Lean correctness proofs over six months, uncovering a high-severity vulnerability that could allow fund theft.
Bend, a language that proves the accuracy of AI implementations by declaring rules in code, has been released, offering C-level performance on CPUs and GPUs.
OpenAI completed a Lean 4 formal proof of the Navier-Stokes equations, reducing verification costs to approximately 1/10 of previous estimates.