Software can pass its tests and still contain a dangerous mistake. &Truth, a company based in Palo Alto and Singapore, has emerged from private development with $70 million in early funding to automate mathematical checks of software. It is building a system intended to show that code follows precisely stated requirements, with proofs that other people can check independently.
The approach, called formal verification, has long required expensive expert work. &Truth says AI and its own automation can make it practical more widely, and it plans to share foundational software libraries publicly. The limits of the promise matter: a proof establishes that code meets specified requirements under stated assumptions. Turning a business's often imprecise wishes into those exact requirements is itself part of the product the company is building.
Source · andtruth.com ↗
