Frege
Neural networks are being deployed into systems where their behavior has to be known.
Formal guarantees have existed only for small models, far below the scale of real deployment.
Frege is a formal verification system for neural networks. It produces mathematical proofs that a deployed model stays within specified bounds, for every input in a named set, on models with billions of parameters.
Every result is a Lean proof that can be checked by anyone, independently.
We think formal verification is how AI earns a place in the many systems that cannot fail, from aviation to medicine to critical infrastructure.