&Truth launches AI-assisted formal verification company

&Truth emerged from stealth on Thursday as a public benefit corporation developing AI-assisted formal verification, a mathematical method for checking whether code satisfies precisely stated properties. The company said it raised $70 million in seed funding. Its announcement did not identify a generally available product, customer deployments, pricing or supported programming languages.

The startup says it is building what it calls a universal verification machine that could read code in any programming language and produce independently checkable proofs. The announced scope is a product ambition rather than a capability demonstrated by the evidence released with the launch.

Formal verification turns a description of what software must do into mathematical obligations, then checks proofs that the code meets them under stated assumptions. It can provide stronger guarantees than ordinary testing for the properties examined, but it does not establish that a specification captures every real-world failure mode. Faulty assumptions, user mistakes and hardware failures can remain outside the proof.

The concrete research result behind the launch is narrower. In an August CryptoProver preprint, researchers described an AI-based system that generated internal specifications and Verus-checked proofs for production cryptographic libraries from fixed top-level API contracts. The paper says CryptoProver constructed an independent proof for curve25519-dalek without changing executable code, using a fixed trusted library of field specifications, arithmetic facts, axioms and standard-library components. The run took 11.4 hours and incurred $466.99 in recorded API costs.

The paper also says CryptoProver verified RustCrypto chacha20 version 0.10.1 against a human-authored specification based on RFC 8439. That experiment covered the portable backend, not SIMD backends. Neither result demonstrates a verifier that works across arbitrary programming languages or unrestricted codebases.

The research documents why mechanically checked safeguards matter when AI helps construct proofs. An early prompt-only version claimed 97.1% completion, but an audit found 11 proofs that depended on invented axioms and five cases that broke sibling modules. The researchers then added acceptance gates designed to reject weakened specifications, invented axioms and cross-module breakage.

&Truth says AI can accelerate formal verification by 100 times or more and that its proof automation can add another 100-fold gain. The company did not tie those broad multipliers to a general benchmark or reproducible product evaluation in its launch materials, and it did not disclose the investors or terms behind the reported seed round.