Zum Inhalt springen
Introspectum
Anfragen
Menü
Anfragen

Software Factory

Baut aus Ihrem Code und Ihren Dokumenten einen Graphen, lässt KI-Agenten darauf arbeiten und prüft ihre Änderungen mit formaler Verifikation.

Für Softwareteams, die Code mit KI schreiben und dafür geradestehen müssen, zuerst für Start-ups und kleine IT-Unternehmen.

EintragenAnfragen
Satz 129 in Gottlob Freges Begriffsschrift: eine Formel als Baum aus Linien, ihre Bedingungen verzweigen sich von einem Urteilsstrich aus.
Gottlob Frege, Begriffsschrift, 1879. Library of the Institute of Mathematics, Polish Academy of Sciences.

So funktioniert es

Die Software Factory liest Ihren Code und die zugehörigen Dokumente in einen Graphen ein: Anforderungen, Entwurf, Tests, Fehlerberichte und Analyseergebnisse, jeweils verknüpft mit dem Code, den sie betreffen. Der Graph baut auf dem Code-Property-Graph1 auf, der Syntax, Kontrollfluss und Datenfluss eines Programms verbindet. Sie sehen ihn als Architekturkarten nach dem C4-Modell2, vom ganzen System bis zu einzelnen Funktionen.

Auf dem Graphen arbeiten KI-Agenten in Schritten nach ISO/IEC/IEEE 152883, der Norm für Prozesse im Systemlebenszyklus. Ein Sprachmodell schreibt nur, was ein Beweis prüfen kann: Funktionsrümpfe zu Spezifikationen, die Menschen freigeben. Codegerüste, Tests und Dokumente entstehen ohne Modell aus dem Graphen, jedes Mal auf dieselbe Weise.

Formale Verifikation prüft jede Funktion gegen ihre Spezifikation, mit den Verifizierern Prusti4 und Verus5. Schlägt ein Beweis oder ein Test fehl, geht das Gegenbeispiel zurück an das Modell, bis beide bestehen oder ein Mensch übernimmt. Jeder Schritt hinterlässt einen Prüfpfad.

Die Presse ist das Modell, das versiegelte Gewicht die Spezifikation, die Waage der Beweis.

Stand der Entwicklung

Sie liest Rust, C und TypeScript. Am 4. September 2026 las sie ihren eigenen Code, 113 Rust-Dateien, in 4,8 Sekunden in einen Graphen mit 12.801 Knoten ein, und die 95 Dateien von ripgrep6 in 7,3 Sekunden in 20.049 Knoten. Wiederholte Läufe mit demselben Code ergaben dasselbe Ergebnis.

Die Verifikation läuft durchgängig mit Prusti und Verus, bisher an kleinen Programmen wie einem Ringpuffer und der Alarmlogik eines Rauchmelders.

Für ein Audit exportiert sie eine Rückverfolgbarkeitsmatrix und einen Sicherheitsnachweis in der Goal Structuring Notation7. Ein Zertifikat stellt sie nur aus, wenn die Verifizierer gelaufen sind, jede Beweisverpflichtung erfüllt ist, jeder Test besteht und jede Anforderung rückverfolgt ist.

Sie liest und schreibt Anforderungen nach IEEE 8308 und Entwurfsbeschreibungen nach IEEE 10169 und erzeugt aus dem Code UML-, SysML- und Mermaid-Diagramme.

Als Nächstes bauen wir darauf den Agentenprozess.

Warteliste

Hinterlassen Sie Ihre E-Mail-Adresse, um das Produkt Software Factory vor dem Start zu testen.

Was wir speichern und warum, steht in der Datenschutzerklärung.

Quellen

  1. 1Fabian Yamaguchi, Nico Golde, Daniel Arp, Konrad Rieck: Modeling and Discovering Vulnerabilities with Code Property Graphs. IEEE Symposium on Security and Privacy, 2014.
  2. 2Simon Brown: The C4 model for visualising software architecture.
  3. 3ISO, IEC, IEEE: ISO/IEC/IEEE 15288:2023, Systems and software engineering: System life cycle processes. 2023.
  4. 4Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers: Leveraging Rust Types for Modular Specification and Verification. Proceedings of the ACM on Programming Languages, OOPSLA, 2019.
  5. 5Andrea Lattuada et al.: Verus: Verifying Rust Programs using Linear Ghost Types. Proceedings of the ACM on Programming Languages, OOPSLA, 2023.
  6. 6Andrew Gallant: ripgrep. GitHub.
  7. 7Assurance Case Working Group: Goal Structuring Notation Community Standard, Version 3. Safety-Critical Systems Club, 2021.
  8. 8IEEE: IEEE 830-1998, Recommended Practice for Software Requirements Specifications. 1998.
  9. 9IEEE: IEEE 1016-2009, Standard for Information Technology: Systems Design: Software Design Descriptions. 2009.