Fourteen proven cores: five Canadian government libraries, and dpkg's version ordering

General
1

Some of you helped me with a cumulative-product proof last week. Here is what it was for.

Two repositories, both public, both re-checkable with a four-line project file.

Ten cores* from five open-source libraries published by Canadian federal bodies — the National Research Council, Environment and Climate Change Canada, Statistics Canada, and ISED’s Communications Research Centre — across Mortran, C and Fortran. 169 obligations, none unproved, none justified. 50 functional contracts, 73 run-time checks, 46 termination.

Four cores for the Debian version-ordering rules, written from Policy 5.6.12 rather than from dpkg’s C. 63 obligations, none unproved, none justified. 38 functional contracts, 4 run-time, 21 termination.

Each core was proved locally, then re-proved independently on a second machine of different architecture and toolchain before it was admitted.

Solver grades, since a clean total invites the question. Run with one back end at a time: the Canadian set is not 3/3 — Z3 alone proves all 169, cvc5 alone misses one, Alt-Ergo three, and the three fragile checks are named in the README. The dpkg set is 3/3; all three provers discharge all 63 alone.

What is deliberately not proved is in both READMEs rather than left to be found. The dpkg set is the sharper example: it is not verrevcmp. No epoch/upstream/revision split, no interleaving of numeric runs, strings fixed at 64 characters. Walk’s contract pins the result when the current characters differ and does not state the all-equal case; Run_Length states its zero case and an upper bound but not that it counts the run. Both are implemented and unspecified, and the README says so.

The Ada was machine-generated by a 27B open-weight model running locally, then checked by gnatprove. The repositories say that before they say anything else. The four dpkg cores took eight rounds between them — one right first time, the others two, two and three.

I would be glad of holes being found in any of it. That is rather the point of publishing the sources rather than the numbers.

* “Core” is our own word rather than a SPARK one, and I have used it throughout, so: one package specification, small enough to prove in a single sitting, carrying the contracts for the properties it claims. Each is proved, then re-proved from the source alone on a second machine before it is recorded. You would just say “package”, and you would be right — I have kept our word because the repositories use it.

2

I think I speak for most people when I say that I’d rather see your own writing instead of a pile of LLM generated slop that obscures whatever you’re trying to say behind so many meaningless sentences that it becomes impossible to figure out what it is.

Also did you even bother to look at this LLM output before you posted it here?

Every function here carries a Post

This is blatantly untrue if you bothered to even glance at the code. Most functions do not have a Post or prove much of anything.

3

Well I only speak for me but its a request for people if interested to verify the proofs. Yes I did read it and quite heavily edit it. I’ll put an advisory at the top of each post. I often mix up the word function and core, which is a personal term used to identify a proven mechanism, which accidentally entered the forum, so I tried to explain that. (One of the edits I made when I uncarefuly examined the post). Regarding the code, its all about the code, and several AI agents were unfortunately executed as a product of this complaint.

4

My issue is not specifically with a LLM writing it but instead with all the meaningless fluff that obscures what you’re actually trying to say as well as the extraordinarily obnoxious Claude writing style.

Let’s take the first paragraph:

Ten cores* from five open-source libraries published by Canadian federal bodies — the National Research Council, Environment and Climate Change Canada, Statistics Canada, and ISED’s Communications Research Centre — across Mortran, C and Fortran. 169 obligations, none unproved, none justified. 50 functional contracts, 73 run-time checks, 46 termination.

This doesn’t actually tell me anything about what you’ve done aside from writing something using SPARK, it’s all just useless noise because the reader does not have whatever context the LLM did. You could instead write “I’ve experimented with using a LLM to extract 10 one-liner functions and write some properties surrounding them, here’s the results.” That sentence would make it so much easier to understand what you’re trying to present.

You could then follow it up with your own analysis of what properties the LLM proved since the most notable thing from the looking at the code is that there’s a lack of anything really useful here. For example, in Banff_Prorate_Pkg‎ there’s all these properties defined (Conserved‎, Shortfall_Is_Bounded, No_Component_Exceeds_Total), however they’re never actually used so nothing is actually proven about the main function (and I’m not sure they would prove anything useful if they were used anyway).

5

You’re really good at this, thats really helpful - thank you. I’m going to have another look and see if there s a solution

6

Agreed.
One is at a loss trying to understand the topic line alone.