Skip to content
Introspectum
Email us
Menu
Email us

Software Factory

Builds one graph from your code & documents, lets AI agents work on it, & checks their changes with formal verification.

For software teams that use AI to write code & must stand behind it, starting with startups & small IT companies.

Join the waitlistEmail us
Proposition 129 in Gottlob Frege’s concept notation: a formula drawn as a tree of lines, its conditions branching from one judgement stroke.
Gottlob Frege, Begriffsschrift, 1879. Library of the Institute of Mathematics, Polish Academy of Sciences.

How it works

The Software Factory reads your code & its documents into one graph: requirements, design, tests, bug reports & analysis results, each linked to the code it concerns. The graph builds on the code property graph1, which joins the syntax, control flow & data flow of a program. You see it as architecture maps in the C4 model2, from the whole system down to single functions.

On top of the graph, AI agents work in steps modelled on ISO/IEC/IEEE 152883, the standard for system life cycle processes. A language model writes only what a proof can check: function bodies, against specifications that people approve. Skeletons, tests & documents come from the graph without a model, the same way every time.

Formal verification checks each function against its specification, with the Prusti4 & Verus5 verifiers. When a proof or a test fails, the counterexample goes back to the model, until both pass or a person takes over. Every step leaves an audit trail.

The press is the model, the sealed weight the specification, the balance the proof.

Where it stands

It reads Rust, C & TypeScript. On 4 September 2026, it read its own code, 113 Rust files, into a graph of 12,801 nodes in 4.8 seconds, & the 95 files of ripgrep6 into 20,049 nodes in 7.3 seconds. Repeated runs on the same code gave the same result.

Verification runs end to end with Prusti & Verus, so far on small programs such as a ring buffer & the alarm logic of a smoke detector.

For an audit, it exports a traceability matrix & a safety case in the Goal Structuring Notation7. It issues a certificate only when the verifiers ran, every proof obligation holds, every test passes & every requirement is traced.

It reads & writes requirements in the form of IEEE 8308 & design descriptions in the form of IEEE 10169, & draws UML, SysML & Mermaid diagrams from the code.

Next, we build the agent process on top of it.

Waiting list

Leave your email address to test the Software Factory before its release.

Read what we store & why in the privacy policy.

Sources

  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.