Better software.
With proof to back it up.

Give useful software a firmer foundation.

A software test asks whether a program works on a particular example. A mathematical proof can establish that a defined rule holds across every input within its stated scope. Bringing more of that certainty to the open-source libraries behind everyday software is an encouraging, practical advance.

In an October 22 research report, Anthropic described a collaboration with Theorem that used Claude to prove security properties of compiled programs from more than 100 real-world libraries.

For readers following Super Intelligence (SI), the useful development is the division of labor: a model does the laborious proof-writing, while a separate proof checker checks the mathematics. The result is more than a model saying its own answer looks right.

Start with the tests developers already have.

The team began with entry points used by Google’s OSS-Fuzz project, which feeds programs large numbers of generated inputs to find crashes. Existing tests were converted into formal specifications: precise statements about what a compiled program must do.

According to Anthropic’s report, over a few weeks Claude patched bugs it encountered and then proved no-crash properties for 239 entry points across 123 libraries. The proofs concern compiled RISC-V machine code and comprise about 180 million lines in Rocq, a formal proof system.

The large line count is not the interesting part by itself. The useful change is that a specialist technique, once exceptionally labor-intensive, can be applied across many existing projects without asking each developer to handwrite an enormous proof.

There is also a practical feedback loop. When a proof fails because a program violates the specification, investigating that failure can reveal a bug. The team reports finding and patching bugs during the effort, then proving properties of the patched program—not pretending a proof erased a defect in the original.

A strong guarantee needs a clear boundary.

The reported proofs establish that the selected tests do not crash for inputs smaller than 64 MB under a particular model of execution: single-threaded, statically linked RISC-V programs using musl libc on Linux, with a fixed memory budget.

Those conditions matter. As the researchers explain, the work does not prove that an entire library is free of every bug, or that the same guarantee automatically applies to an ordinary x86 or ARM installation. The theorem statements, the mathematical models of the processor and operating system, and Rocq’s proof checker remain trusted foundations.

That is the point of being precise: readers and developers can see exactly what has been established and what a future implementation would need to cover. These are concrete software properties, not a claim of general-purpose SI or GSI.

Make the next proof easier to write.

Anthropic and Theorem have released a subset of the proofs and their theorem statements for others to inspect and check. Theorem also outlines a longer-term roadmap for a verified software stack; that broader stack is an ambition, not a completed result.

Proofs can be reused much like code. Establish a useful building block once, and another project may be able to build on it rather than start from an empty page.

Our view: this is a particularly constructive use of SI-assisted development. Better tools for checking the shared libraries that software depends on could make reliable engineering more accessible. The near-term win is specific and tangible: more machine-checked guarantees, attached to clearly stated claims, for real open-source programs.