Been a while since I last updated the project. For those who have not heard of the project before it is basically a crdt library for Ada as an Alire crate.
Canonical source has been moved to GitHub due to TOS changes on Codeberg pertaining AI assisted code (their phrasing is a bit vague but I do not want to take chances here).
The code is human driven, we have made good progress on getting our code to DO-178C DAL-C.
Fancy words for High Level Requirement tracking with compliance artefacts and stuff.
Code is mostly proven with SPARK with a few remaining exceptions to get to. We are around SPARK Gold proof robustness wise at the moment.
API docs has been better updated to include details on SPARK coverage, as well as noting deprecated features.
Earlier post on 1.1.0 release: Crdt version 1.1.0
tldr changelogs:
Clock strategy selection (Lamport, Vector, Matrix), V3 wire protocol with clock-kind discriminator, clocked sync layer, generic LWW sets, SPARK proof expansion, and documentation modernization.
Full changelogs: Ada_CRDT/docs/changelogs/crdt-1.7.0.md at 872831b287074dbe204bcb629ac3de2344eb8fd7 · bladeacer/Ada_CRDT · GitHub
Alire Crate URL: Alire - Crdt
P.S. 1.7.0 PR might take a while to be merged upstream.