Formal methods, put to work
Proved,
not just plausible
Formal methods have come of age, thanks to a growing community:
proving that a system does what it should is now within reach, and
we think everything deserves a theory.
We start with simple, focused tools: for long-lived systems,
for formal mathematics, and for rules languages.
polis: your long-lived systems, understood
polis gives your whole COBOL ecosystem an exact meaning, then explains it, assesses it, improves it and modernizes it to Java, all deterministically. In a loop with it, AI becomes verifiable: every proposal is checked against the original. So is a migration: its correctness checked against the code it replaces, whether the Java was written by a vendor or by an AI.
Discover polis Formal mathematics Coming sooncanode: mathematics, wherever it lives
CA is our proposal for content addressing in Lean: every result gets an address computed solely from its content. We use it for all the Lean we work with. canode, a CA node, is our tool for formal, decentralized mathematics. Build on any result by its address, whoever proved it. A live node is open: Mathlib, Lean Pool and Tau Ceti, by content.
Explore the mathematics Rules languages Early alphaattesta: what your rules really catch
attesta checks the correctness of detection rules and filter configurations: each gets an exact meaning and is held against what it was meant to catch. What a rule catches, what it misses and what changed between two versions comes with its evidence. And deterministic: the same rules give the same report, byte for byte, on any machine.
Meet attestaShared ground
All three tools stand on Lean: from what is written in it, Lean builds proof objects that its small kernel verifies. We use it twice: as the language in which mathematics, software and rules get an exact meaning, and as a language we write part of our tools in.
01 Meaning
A meaning in a formal logic
A theorem, a program or a detection rule is given an exact meaning in Lean, a formal logic. Once it has one, questions about it have answers that can be checked.
02 Checking
A checker, not a hunch
A proof checker decides what holds. What it cannot decide is said plainly, with its reason, and never dressed up as a result.
03 AI
Verifiable AI
Language models propose and explain; the checker decides. Prose a model writes is marked as prose and is never counted as evidence.
Mathematics has a method older than any computer: definitions say exactly what things are, each theorem comes with its proof, and a theory is many of them, built on one another. Formal mathematics now has a machine check it all. We work toward software engineering built the same way.
The companyJust getting started
Proofinity is an Italian company, built from Milan and Rome.
Follow along on GitHub, where our open‑source Lean libraries live, and on LinkedIn.