We spoke about this on the Ada SPARK Office Hours last Friday (recording to follow). The team at AdaCore has built a demonstration project to highlight how deterministic tools with Ada SPARK can be used to build trust in AI generated artifacts.
There is a blog post with details.
The repository is here:
I am biased of course, but I think the content is very interesting. It is a full implementation of a traffic light control system. Not full as in, use in a real intersection, but full as in starting from requirements in a concept of operation, to high-level requirements, to low-level requirements, to code, tests, code coverage and all cross-linked with full traceability.
The repository has full automated test and is AI enabled (see .claude and .codex directories). There is a demo-prompt that you can execute to add new requirements to the implementation and the guardrails will make sure that the resulting code is trustworthy.
Have a look at it and dig into the details. The community tools are fully supported of course. You will need to bring your own AI subscription. The open models are not supported yet, will be experimenting with that myself as well.
We are very interested in feedback and to learn how you could use this to build your own control systems with high-integrity.
Like-and-subscribe!
Regards,
Mark