Verify the Contract Before You Verify the Work
TL;DR for operators A deterministic verifier can tell you whether an artifact satisfies a formal specification. It cannot tell you whether that specification faithfully represents what the user originally asked for. Magenta makes this distinction explicit. The system first converts a natural-language mathematics problem and proposed answer into a Lean statement, then uses a learned judge to check whether that statement preserves the intended problem before attempting a machine-checked proof. When proof verification fails, another judge classifies the failure as mathematical or formal-implementation related and sends the next correction to the corresponding component.1 ...