&Truth emerged from stealth on October 29 with $70 million in seed funding and plans to automate both software proofs and the work of turning business goals into the mathematical requirements those proofs check.
Its planned tools target developers and enterprise teams working with legacy and AI-generated code. The company is building on Lean, an open-source proof system, with the aim of producing proofs that anyone can check. Each proof would establish a specific claim about code under stated assumptions.
Founded in early 2026, the public benefit corporation has headquarters in Palo Alto and Singapore and plans to expand its Singapore research, engineering and commercial teams. Its announcement did not name investors or disclose a valuation.
A separate paper revised on October 16, coauthored by &Truth's Chuyue Sun and co-CEO Clark Barrett, reports that CryptoProver generated a proof for curve25519-dalek, a cryptographic library used in Signal. Using the Verus verification tool, the run took 11.4 hours and incurred about $467 in recorded model API charges.
Humans supplied the requirements, mathematical inputs and proof order before timing began. The authors limit the result to compliance with those requirements, excluding cryptographic security and resistance to side-channel leaks. They also caution that their favorable choice of libraries may overstate performance on unfamiliar code.