When we started experimenting with e-Orzecznik around 2023, the team already had an Agda formalization of its procedure language. That was a good head start. Getting it into the developers’ everyday work was the next job.

e-Orzecznik makes software for occupational medicine in Poland. Its procedures cover examinations for employees, drivers and other groups, along with the forms and documents those examinations produce. This is the setting for the work described here: the people developing those procedures, and the rules they have to keep straight as the software changes.

One examination, several documents

The user manual gives a feel for the dependencies. An examination starts with a procedure, a patient, an employer and a job. The examination card supplies information to the certificate; issuing it also creates an entry in a register. Editing a completed examination can change the certificate’s contents and require fresh signatures. A form is part of a longer piece of work.

The developers had put the procedure logic in a dedicated language: a restricted subset of JavaScript with its own semantics and validation rules. Around 2019, they modeled its syntax, meaning and restrictions in Agda. That model helped with specification, analysis and language design. It was separate from the production runtime.

By the time we began working together, there were tens of procedures, hundreds of fields and rules reaching across document boundaries. The language gave that complexity some structure. Testing still took a great deal of time—by the team’s account, sometimes more than implementation.

Giving the model a daily job

Knowing precisely what the language means is a starting point. You still have to show that a particular procedure does what you require of it. We began stating those requirements over the existing semantics and proving them for concrete procedures.

For example, a requirement might say that a document cannot be produced until certain conditions involving other documents hold. That is an illustration of the kind of property involved, rather than a report of a fault we found. Writing it down precisely gives the proof work a definite target.

LLM assistance made some of the tedious proof work practical to attempt. Work that had been economically unattractive to do by hand became worth doing. The division of responsibility stayed straightforward:

The assistant could propose a proof. Agda still had to accept it.

There was a less glamorous job before that: agreeing on the statement. Codex Scribe helped translate requirements from natural language into Agda. Its deterministic readback then rendered the formal statement in semi-natural language for review. A perfectly well-formed statement can still say the wrong thing. Someone has to read it and decide whether it captures the requirement they meant.

We brought this into the interactive tool e-Orzecznik already used to develop procedures. MLTTDB served as the dependently typed term store. The store keeps the terms; the proof assistant checks them against their declared types. That split let the team work with editable formal data without asking the database to decide whether the data was semantically valid.

The next revision is where it gets interesting

The product’s release notes show how this work keeps moving. Examination-card entries can feed documents for the patient and their primary-care doctor. Templates change; signature requirements change. The 2026 updates include both. These are ordinary maintenance tasks, with dependencies attached.

In the development tool, a revision could cause a previously accepted proof to stop checking. That gave the developer something specific to investigate. Perhaps the change broke a requirement. Perhaps the requirement had deliberately changed. Sometimes the proof itself needed repair. The team made that decision, used assistance where it helped, and re-established the properties they needed.

The project team reports that difficult interactions between rules became much easier to detect. A failed check gave them a reason to look closely at an edit, including edits whose consequences were otherwise hard to see.

What changed for the team

The team’s estimate for overall development time was substantial:

A new procedure took at most one-fifth of the previous development time.

e-Orzecznik also reports roughly one-eighth of the previous manual testing time, with substantially fewer test cycles. These measure different parts of the work; they should not be multiplied together. When demand increased, the workflow enabled the team to double monthly procedure output. Demand was part of that result too.

These are the project team’s operational estimates, rather than an independently controlled benchmark. They describe this development workflow, with the existing formalization and the team’s knowledge of its own procedures.

There is a limit to the proof claims as well. They establish the stated properties in the formal model, under its definitions and assumptions. Showing that the production implementation follows that model is a separate obligation. We do not get that result merely because a procedure’s proof checks.

What we did get was a way to return to explicit claims as the procedures changed. The earlier Agda work supplied the language’s meaning. It could now help with the next edit, too.