oss-verify

클로드가 오픈소스에 수학 증명을 쓰다 찾은 버그 수백 개 앤트로픽이 클로드로 오픈소스에 「64MB 미만 어떤 입력에도 안 죽는다」는 형식 검증 증명을 쓰다 버그 수백 개를 찾았고, 라이브러리 123곳의 진입점 239개는 몇 주 만에 증명까지 끝냈다고 2026년 10월 22일 발표했습니다. - 앤트로픽, LLMs are making formal software verification feasible at a much larger scale(2026.10.22) anthropic.com - 같은 글 부록(PDF) www-cdn.anthropic.com - X @AnthropicAI(2026.10.23 한국 시간) x.com - NVD CVE-2026-56132(libexpat) nvd.nist.gov - Theorem 증명 공개 theorem-labs/oss-verify-proofs - Theorem OSS Verify theorem-labs/oss-verify - 해커 뉴스 글(2026.10.23) news.ycombinator.com - 해커 뉴스 댓글: news.ycombinator.com , news.ycombinator.com , news.ycombinator.com - 긱뉴스 한국어 요약 news.hada.io

@rajashree so so good. this page is great github.com/theorem-labs/oss-verify/blob/main/docs…

I recommend reading what the "proof" actually provides: github.com/theorem-labs/oss-verify/blob/main/docs… Yes, it's better than what we have, but not "proven bug free". And it's definitely not happening on $100M. Show me one large app proof-hardened, and the cost. Say, LibreOffice. Heck, just nginx.

El artículo de Anthropic, con los detalles y las pruebas publicadas: anthropic.com Y si quieres probarlo en tu código, Theorem ha publicado una skill de Claude: github.com/theorem-labs/oss-verify/blob/main/.cla…

Model: theorem-labs/rocq-linux-process-semantics based on mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: theorem.dev , theorem-labs/oss-verify , theorem-labs/oss-verify-proofs