Logical Intelligence’s Aleph Leads Formal Verification Benchmarks

Logical Intelligence announced in a press release that its AI coding agent Aleph achieved leading results on four formal reasoning benchmarks, including PutnamBench, VeriSoftBench, LeanEval, and Verina. The company stated that Aleph’s performance demonstrates that formally verified code generation is now practical for critical infrastructure software.

Aleph solved 99.4 percent of the PutnamBench problem set, outperforming ByteDance’s Seed-Prover 1.5 at 86 percent and Hilbert at 69 percent. On VeriSoftBench, which measures real world software verification, Aleph reached 94 percent success, ahead of Harmonic’s Aristotle at 69 percent and Google Gemini-3 Pro at 65 percent. It also achieved top results on LeanEval and a perfect score on Verina, which was independently confirmed by benchmark authors.

The company said Aleph operates in environments requiring machine checkable proofs rather than probabilistic outputs. It is already being used in production verification workflows, including work involving the Ethereum Foundation’s ArkLib cryptographic libraries. Logical Intelligence plans to open a beta program for Aleph later this year.

Aleph automates formal verification and produces proofs that ensure critical logic functions correctly across all execution paths. The agent is intended for operators of infrastructure and safety sensitive systems who require verified code generation.