LLMs are making formal software verification feasible at a much larger scale

Anthropic researchers, in collaboration with Theorem, demonstrate that large language models like Claude can autonomously produce formal correctness proofs for real-world software at an unprecedented scale. Working at the RISC-V assembly level, Claude generated proofs for 239 entry points across 123 open-source OSS-Fuzz libraries—roughly 180 million lines of Rocq proof code—showing that these binaries never crash on any input under 64 MB. The process also uncovered hundreds of latent bugs that had evaded years of fuzzing, including a counter underflow requiring a rare ~20 MB input layout and a rediscovery of a deep-nesting CVE in libexpat. The authors describe additional case studies (proving zlib's Linux kernel implementation against RFC 1950, verifying a Rust Python interpreter against CPython semantics, and auditing a PDF reader) and note falling costs as newer models need ~40% fewer tokens and proof reuse cuts token use by ~17%. They stress that "formally verified" does not mean "bug-free," since proofs only guarantee conformance to a spec and its machine model, and outline limitations around threading, architectures, and incomplete coverage. 

https://www.anthropic.com/research/formal-verification

Comments

Post a Comment

Popular posts from this blog

OWASP ASVS 5.0 Released - Key Updates and What You Need to Know

The OWASP Foundation has released version 5.0 of the Application Security Verification Standard (ASVS), a major update to their security framework for web applications. This new version features restructured security requirements for better clarity, expanded guidance for cloud and API security, improved DevSecOps integration for CI/CD pipelines, updated threat modeling support, and enhanced compliance mapping with standards like NIST and PCI DSS. ASVS serves as a critical benchmark for developers building secure applications, penetration testers conducting security assessments, and auditors performing compliance reviews.  The standard is available for download from the OWASP ASVS project page, with organizations encouraged to integrate it into their software development lifecycles through code reviews and security testing tools. As a vendor-neutral, community-driven project, OWASP continues to welcome contributions to further develop the standard. This release represents an importa...
Read more

Critical OpenSSH Flaws Enable MITM and DoS Attacks

On February 18, 2025, HackRead reported on two critical vulnerabilities in OpenSSH, identified by the Qualys Threat Research Unit (TRU). The first vulnerability, CVE-2025-26465, affects the OpenSSH client and permits machine-in-the-middle attacks, potentially allowing attackers to impersonate legitimate servers and compromise SSH session integrity. This flaw exists regardless of the 'VerifyHostKeyDNS' setting and has been present since OpenSSH version 6.8p1. The second vulnerability, CVE-2025-26466, impacts both the client and server, enabling pre-authentication denial-of-service attacks that consume excessive system resources, leading to potential outages. Introduced in version 9.5p1, this issue persists up to version 9.9p1. Users are strongly advised to upgrade to OpenSSH version 9.9p2 to mitigate these vulnerabilities.  https://hackread.com/critical-openssh-flaws-expose-users-mitm-dos-attacks/
Read more

MITRE ATT&CK v19 Redefines How Defenders Model Modern Threats

MITRE ATT&CK v19 introduces one of the framework’s most significant structural changes in years, splitting the former Defense Evasion tactic into two clearer categories: Stealth and Defense Impairment. The release also expands coverage for AI-enabled adversary behavior, social engineering, and mobile detection strategies, while adding greater precision to ICS through new sub-techniques. Beyond taxonomy updates, v19 signals a broader evolution of threat modeling—toward more actionable, behavior-driven intelligence that reflects how attackers increasingly blend automation, deception, and cross-domain operations.  https://medium.com/mitre-attack/attack-v19-ff329cb65d66
Read more