Formale Verifikation in Marketing-Modellen: warum Lean 4 die Compliance-Frage löst

In der Software-Entwicklung gibt es seit Jahrzehnten eine kulturelle Übereinkunft, dass Code via Unit-Tests, Integration-Tests und End-to-End-Tests abgesichert wird. Diese Tests prüfen Beispiele: Wenn die Eingabe X ist, muss die Ausgabe Y sein. Wer eine Million solcher Beispiele durchläuft, hat eine hohe statistische Konfidenz, dass die Software korrekt funktioniert. Aber Statistik ist nicht Beweis. Es bleibt immer eine endliche Anzahl von Tests, und Edge-Cases können durch die Maschen rutschen. Genau diese Lücke schliesst eine andere Disziplin, die in den letzten fünfzehn Jahren aus der akademischen Nische in die industrielle Anwendung gewandert ist: formale Verifikation.

Formale Verifikation beweist Eigenschaften eines Programms für alle möglichen Inputs. Statt zu fragen 'funktioniert mein Code bei diesen tausend Beispielen', fragt sie 'ist diese Eigenschaft mathematisch garantiert, egal welcher Input kommt'. Werkzeuge dieser Disziplin sind Theorem-Prover wie Coq, Isabelle, Agda — und seit etwa 2021 Lean 4, ein moderner Prover aus Microsoft Research, der mathematische Beweise und Software-Verifikation in einer einzigen Sprache vereint. Lean 4 hat sich in der akademischen Mathematik schnell etabliert (das Projekt Liquid Tensor Experiment hat damit einen Theorem von Peter Scholze formal verifiziert), und ab 2024 zunehmend in Industrie-Anwendungen — von kryptografischen Bibliotheken bei Cloudflare bis zu Smart-Contract-Verifikation in DeFi.

Für regulierte ML-Anwendungen ist diese Methode strategisch interessant. Stellen wir uns vor, ein Marketing-Mix-Modell empfiehlt einer Schweizer Bank, das Display-Budget um 23 Prozent zu erhöhen und das Print-Budget entsprechend zu reduzieren. Die Bayesian-Pipeline hinter dieser Empfehlung läuft mit MCMC-Samples, Floating-Point-Arithmetik und Channel-Interaction-Effekten. Der Compliance-Officer fragt: 'Können Sie mir garantieren, dass die Summe der empfohlenen Budgets genau der Summe der aktuellen Budgets entspricht? Können Sie garantieren, dass keine negative Empfehlung entsteht? Können Sie garantieren, dass gleicher Input plus gleicher Seed bit-identische Outputs produziert?' Diese drei Properties — Budget-Conservation, Non-Negativity, Determinismus — sind genau die Art von Eigenschaften, die ein klassischer Unit-Test nur stichprobenartig prüfen kann, ein Lean-4-Theorem aber für alle möglichen Inputs beweist.

Ein konkretes Theorem aus dem MMM-Wizard-Verification-Repository macht das anschaulich. Die Funktion `runMmm` nimmt Input-Daten und einen Seed entgegen und produziert eine Recommendation. Das Theorem `budget_conservation` lautet: für jede ChannelAllocation `alloc` und jede daraus berechnete Recommendation `rec` gilt `alloc.totalSpend = rec.totalRecommended`. Der Beweis verwendet algebraische Manipulationen über die internen Datenstrukturen, die Lean 4 maschinell prüft. Wenn ein Entwickler später den Meridian-Service-Code ändert und versehentlich eine Floating-Point-Akkumulation einführt, die den Budget-Total um 0.0001 Franken erhöht, schlägt der `lake build`-Lauf in der CI-Pipeline fehl. Der Beweis bricht. Der Merge wird blockiert. Das ist ein qualitativ anderes Sicherheitsniveau als ein Test, der zufällig diese spezifische Floating-Point-Welle nicht trifft.

Warum ist das für regulierte Industries qualitativ wichtig? Drei Gründe. Erstens die Compliance-Logik: nDSG Art. 22 und DSGVO Art. 22 verlangen Erklärbarkeit automatisierter Entscheidungen. Ein machine-checked Lean-4-Beweis ist die belastbarste Form der Erklärbarkeit, die ein Software-Vendor anbieten kann — robuster als 'wir haben tausend Tests', robuster als ein Code-Review-Approval. Zweitens das Audit-Argument: wer in einer Bank eine Marketing-Empfehlung gegen einen internen Audit verteidigen muss, kann den Lean-4-Beweis als Anhang zum Audit-Report mitliefern und auf eine maschinelle Prüfung verweisen, die unabhängig von menschlichem Code-Reviewer-Urteil läuft. Drittens das Investor-Argument: für VCs und Strategic-Investors, die ML-Companies bewerten, ist machine-checked correctness ein Differenzierungsmerkmal gegen Generalist-Plattformen, die auf 'wir haben gute Tests' setzen.

Diese Methode ist nicht neu — neu ist die Übertragung auf Marketing-Modelle. Cloudflare, AWS und Google verwenden formale Verifikation seit Jahren für kryptografische Bibliotheken und Konsens-Protokolle. Nexbid, eine Schwesterplattform innerhalb der opua-Brand-Family, hat siebenundvierzig Lean-4-Theoreme für ihre Auction-Engine im Repository `protocol-commerce` formal verifiziert. Diese Theoreme decken Eigenschaften wie Truthfulness der Auction, Pareto-Effizienz, Revenue-Equivalence und Manipulation-Resistance ab. MMM-Wizard übernimmt jetzt das gleiche Pattern für Budget-Allokation: das Verification-Sub-Repository wird mit sechs bis acht Kern-Theoremen ausgestattet, die genau die Properties beweisen, die für regulated Industries auditrelevant sind.

Strategisch ist das die mathematische DNA, die eine Brand-Family wie opua zusammenhält. Nexbid verifiziert Auctions. MMM-Wizard verifiziert Budget-Allokation. Mineralis, ein weiteres opua-Tool für Mining- und Energy-Equity-Research, kann das gleiche Pattern auf Equity-Recommendation-Properties anwenden — etwa 'die Empfehlung folgt monoton den fundamentalen Bewertungs-Kennzahlen'. Was wie eine technische Spezialität klingt, ist eine strategische Architektur-Entscheidung: jede Brand innerhalb der opua-Familie nutzt das gleiche Verification-Pattern, was Cross-Brand-Konsistenz, gemeinsame Tooling-Investitionen und einen verteidigbaren USP gegen Generalist-Marketing-Plattformen erzeugt.

Akademisch ist das Pattern bereits validiert. Holger von Ellerts, Mitgründer der opua-Brand-Family und Dozent für KI an Schweizer Hochschulen, hat 2025 an der Hochschule Luzern eine Transferarbeit zu KAN Shadow Scoring und Lean 4 Property Verification für die Nexbid Auction Engine geschrieben. Die Arbeit verbindet zwei Stränge: Kolmogorov-Arnold Networks als interpretable ML-Architektur und Lean 4 als Verification-Layer. Die Übertragbarkeit von der akademischen Anwendung (Auctions) auf produktive Marketing-Anwendungen (Budget-Allokation, Equity-Research) ist nicht zufällig — es ist die strategische Logik, die opua als Brand-Family zusammenhält.

Für CTOs, Compliance-Officers und Tech-Investors, die Software-Vendoren in regulierten Industries evaluieren, sind drei Fragen pragmatisch nützlich. Erstens: Welche Properties prüft Ihre Pipeline maschinell? Wenn die Antwort 'Unit-Tests' ist, ist das Sicherheitsniveau klassisch. Wenn die Antwort 'formal verifizierte Theoreme in einem etablierten Prover' ist, ist das Sicherheitsniveau qualitativ höher. Zweitens: Können Sie die Theoreme im Repository öffentlich einsehbar machen? Open-Source-Lean-4-Files sind eine Form von Trust-Signal, die ein VC oder Compliance-Officer direkt nachvollziehen kann. Drittens: Wie ist die CI-Integration? Ein Theorem-Prover, der nur einmalig läuft und nicht in der CI-Pipeline, bietet keinen kontinuierlichen Schutz vor Refactoring-Wellen.

Wer das Pattern in der Praxis sehen will, kann das öffentliche Repository unter github.com/digital-opua/protocol-commerce einsehen. Die 47 nexbid-Auction-Theoreme sind dort vollständig dokumentiert. Das mmm-wizard-verification-Sub-Repository folgt ab Sprint-6. Beide Repositories sind Apache-2.0-lizensiert, weil opua die Verification-Layer als gemeinsames Schweizer Open-Source-Asset für die Brand-Family positioniert. Wer als Tech-Investor, Compliance-Officer oder Hochschul-Forscher die Methodik tiefer verstehen will, kann sich für ein Audit-Trail-Workshop unter audit@digital-opua.ch anmelden.