# Fourteen proven cores: five Canadian government libraries, and dpkg's version ordering
**URL:** https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723
**Category:** General
**Tags:** spark
**Created:** [September 7, 2026, 8:15pm UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723 "2026-09-07T20:15:39Z")
**Posts on this page:** 6
**Page:** 1
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 7, 2026, 8:15pm UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/1 "2026-09-07T20:15:39Z")
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.
> **[GitHub - the-dark-factory/canada-le-brave: Machine-checked proofs about five open-source...](https://github.com/the-dark-factory/canada-le-brave)**
>
> Machine-checked proofs about five open-source libraries published by Canadian federal bodies. Ten cores, 169 proof obligations, 0 unproved. Sources, receipts and re-check instructions included. The Ada was generated by an AI and checked by a prover — see AI-DISCLOSURE.md.
**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.
> **[GitHub - the-dark-factory/dpkg-version-proofs: Four machine-checked SPARK cores for the Debian...](https://github.com/the-dark-factory/dpkg-version-proofs)**
>
> Four machine-checked SPARK cores for the Debian version-ordering rules (Policy 5.6.12). 63 proof obligations, 0 unproved; all three provers discharge all of them alone. Not verrevcmp, and not a defect report — the README says exactly what is and is not proved. The Ada was generated by an AI and checked by a prover; see AI-DISCLOSURE.md.
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.
---
### Author:  [@liampwll](https://forum.ada-lang.io/u/liampwll)
#### Post date: [September 8, 2026, 10:01am UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/2 "2026-09-08T10:01:26Z")
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.
---
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 8, 2026, 10:34am UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/3 "2026-09-08T10:34:48Z")
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.
---
### Author:  [@liampwll](https://forum.ada-lang.io/u/liampwll)
#### Post date: [September 8, 2026, 11:02am UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/4 "2026-09-08T11:02:17Z")
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).
---
### Author:  [@Tonyg](https://forum.ada-lang.io/u/Tonyg)
#### Post date: [September 8, 2026, 11:29am UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/5 "2026-09-08T11:29:29Z")
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
---
### Author:  [@pmnw](https://forum.ada-lang.io/u/pmnw)
#### Post date: [September 8, 2026, 5:22pm UTC](https://forum.ada-lang.io/t/fourteen-proven-cores-five-canadian-government-libraries-and-dpkgs-version-ordering/4723/6 "2026-09-08T17:22:40Z")
> [@liampwll](#):
>
> 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.
Agreed.
One is at a loss trying to understand the topic line alone.