polis
Formal verification
for COBOL.
The solid ground for understanding,
maintenance, modernization and
AI's creativity.
Deterministic, so the AI that works with it is
verifiable.
- Your COBOL estate programs, copybooks, JCL, DB2 SQL, CICS, IMS, schedules
- Its exact meaning stated for every input, checked by a machine
- Answers you can check the same every time, each with its evidence
polis is about the meaning of a codebase: its formal semantics. It gives the code an exact meaning in Lean, proves what it says, and is deterministic: the same answer every time.
Given, not guessed.
01 Proofs
Proofs, beyond tests
A test tries some inputs; a proof covers them all. Each part of the code is stated for every input and checked by a machine; what cannot be proven is named.
02 Determinism
Deterministic, in the age of AI
The same delivery gives the same answer, on any machine, every time. No model inside the analysis: nothing sampled, nothing to ask twice.
03 Verifiable AI
AI in a loop with a deterministic tool
AI tells the story of the codebase, answers your questions in plain words and proposes changes. polis checks it: the facts it cites come from the analysis, and each proposed change is proven or refused.
04 System
The system, not the language
COBOL is the surface of a whole system: jobs, data sets, DB2, CICS, IMS. polis reads all of it, because modernizing means changing the system, not translating a language.
Not only for the experts.
Everyone who touches the estate reads the same facts, at their own level.
People who do not program
Owners, managers, auditors: the estimate, the risks, plain-language answers. Ask the analysis and get the facts.
IT people new to COBOL
What each program does, in words; business rules as tables; the Java beside the COBOL. No COBOL to learn first.
COBOL experts
The proofs, every case of every paragraph, what a change touches, refactorings proven to change nothing.
From the first estimate
to the new system.
Estimate
On day one: how big, how hard, what is missing. The same numbers every time.
Understand
What every program does, case by case; business rules as tables proven equal to the code.
Assess
What is wrong, missing or fragile, each finding with its evidence, before anyone changes it.
Change safely
What your change touches, and proof, paragraph by paragraph, that it altered nothing else.
Improve
Better COBOL, proposed by polis: each edit kept only where it is proven to change nothing.
Modernize
Services owning their data, Java derived from the model, and your AI's proposals proven or refused.
Check a migration
Java written by a vendor or by an AI, checked against the original COBOL, paragraph by paragraph. Each difference comes with the input that causes it; an error of the COBOL that the Java corrects is told apart from one it carries over; what the Java must never do is checked too; what cannot be decided is named.
What the assessment finds
- cases the code does not handle
- errors nobody checks
- data access the schema would refuse
- programs that misread each other
- code no input can reach
How each finding knows
- proven a theorem about the model, checked by Lean's kernel.
- tested an input was found and run; the model met the problem.
- read the analysis read it from the code and says what it assumes.
Where it runs
On your machines. polis is one command and a container; your code never leaves your site. When it uses a language model, the model runs on your site too.
Fast enough to use
A million lines of COBOL in minutes; a typical application, a hundred programs, in about a minute. Ask, change, ask again: the answer is there before the question goes stale.
You bring the creativity,
polis brings the shoulders.
polis is in alpha, heading to beta. To try it on your own estate, leave your email: we invite a few teams at a time.
You're on the list — we'll be in touch.
Invites go out in small waves; expect a note from a person, not a newsletter machine.