What Does the Software Proof Actually Prove?

Startup &Truth publicly launched on Thursday with a plan to automate formal software verification, Wired reports. The company has raised $70 million. Its effort targets a laborious engineering process that could help developers check AI-generated code, although widespread commercial adoption remains unproven.

Formal verification starts with precise statements about what software must do. Engineers express code mathematically and check whether the code satisfies those statements under specified assumptions. Tests examine selected cases. A proof can establish a stated property across the cases its mathematical model covers.

That distinction gives verification real value. Wired reports that Anthropic and verification startup Theorem used AI to help find open-source software bugs that trillions of tests had missed. Such results support further work. They do not establish that every program can now receive an affordable, comprehensive certificate of correctness. Wired describes the technology as still in the prototyping stage.

The specification creates another boundary. Imagine a system whose requirement permits an employee to retrieve every customer record. A proof that the code correctly implements that permission would not establish that the employee should have it. The requirements document has not earned immunity from mistakes.

For operators commissioning AI-assisted software, the appeal is understandable: restore a dependable connection between an instruction and the resulting program. But describing verified code as simply safe promotes a bounded technical finding into an operating policy. The proof has been offered a management position.

Wired also notes that verification depends on assumptions about how computers and people interact with software. Hardware failures and user mistakes may fall outside a particular model. &Truth’s ambition to eventually cover any programming language is a goal, not evidence of universal coverage. Operators need to know which code, properties, and conditions a check actually addresses.

Before deployment, the commissioning organization should demand the specifications in language its reviewers can evaluate. It should require a record of excluded components, assumed conditions, and unchecked failure modes. It should name who approves the requirements and who orders another review when the code or operating environment changes. The operator’s next decision is not whether to admire the proof. It is whether to authorize the behavior the proof establishes.