This Friday is the next instance of our Ada SPARK Office Hours. There is a slight chance that @sttaft may step in and attend.
Proposed topics:
And of course open to any other topics people are interested to talk about.
More detail and links are here: Ada SPARK Office Hours | AdaCore , 10am-11am ET!
Would pop in for a bit, as it is late in my timezone. Looking forward to it 
Oh man this is early
Good timezones I guess 
Ideal timezone for Germany (thats 4pm in the afternoon here). Added to my calendar! Looking forward to it
Here is the recording from the last Ada SPARK Office Hours, we had roughly 15 people online and had a great discussion.
Discussion on Artificial Intelligence benchmarking, code review, and ecosystem maintenance integrated with strategies for embedded development standards.
Artificial Intelligence Benchmarking Strategy
The benchmarking suite expands to include agentic testing capabilities to better measure self-correction. Developers implemented anti-cheating infrastructure to ensure functionality verification in generated code.
Ecosystem Maintenance and Tools
Teams discussed using automated review tools and maintaining repository health to improve usability. Participants emphasized utilizing Spark specifications to ensure accountability in functional safety systems.
Embedded Design Standard Improvements
Discussions focused on creating stricter design standards for Hardware Abstraction Layer crates and improving crate discovery. Members agreed to leverage automated agents to identify and update documentation issues.
Meeting Welcome and Agenda: The speaker opened the meeting by welcoming participants, including several new attendees, and providing an overview of the discussion topics. They established that this is an open forum where participants are encouraged to raise topics for discussion and introduced the agenda that had been posted on the forum.
AI Benchmarking Suite: The speaker shared an update on benchmarking various AI systems for code generation, noting that while commercial models like Claude’s Opus, Sonnet, and Haiku are used, there is also interest in benchmarking open-weight models. The benchmarking suite, which is publicly available on the AdaCore GitHub under “a_eval,” currently includes approximately 20 challenges, with plans to release more content in the October timeframe.
Benchmarking Methodology: The speaker explained the distinction between “single-shot” and “agentic” benchmarking. In single-shot tests, the AI receives a prompt and must generate code in one attempt, whereas in agentic tests, the AI is allowed to read files and use tools to refine its output. The speaker noted that while single-shot tests measure an AI’s initial understanding, agentic tests demonstrate how well an AI can correct itself, with even smaller commercial models performing well in these scenarios.
Anti-Cheating Infrastructure in Benchmarks: The speaker detailed that the “a_eval” suite includes infrastructure to prevent AI cheating, such as ensuring that the AI provides actual functionality rather than empty functions that satisfy simple pre-conditions. This includes sophisticated tests that verify post-conditions to ensure the implementation is robust and correct.
Property-Based Testing: A participant shared an article regarding property-based testing as a way to prove software correctness when formal verification might be too complex. They noted that this approach could help verify whether specified pre- and post-conditions are rigorous enough to prevent an AI from producing trivial or “null” implementations.
Hardware Testing Costs: The speaker discussed the practicalities of hardware testing, noting that while purchasing dedicated machines might be expensive, it is possible to rent cloud-based high-performance machines, such as AWS instances with Nvidia H100s, for approximately $5 per card per hour to conduct testing.
Deterministic Trust Demo: The speaker announced that the team is working on a public demo, expected in about a month, which focuses on “deterministic trust.” This project aims to build infrastructure around AI that increases confidence in generated artifacts, with a heavy emphasis on Ada and Spark.
Accountability in AI-Generated Code: The group discussed the risks of relying on AI for functional safety systems, emphasizing that humans cannot realistically review large volumes of AI-generated code. Participants agreed that Spark provides a solution by allowing developers to review specifications rather than every line of code, ensuring accountability without requiring exhaustive manual verification.
Model Differences in Context Handling: The speaker noted a significant difference between commercial models and some open-weight models regarding context derivation. When provided with a prompt, commercial models like Opus are better at deriving necessary context and managing multi-step processes—such as running a compiler, prover, and formatter—automatically, whereas open models require more explicit, step-by-step guidance to avoid errors.
AI for Code Review: Participants discussed the use of AI for code review. A participant shared that they use GitLab’s AI-integrated tools, which have successfully identified issues and recognized intent, such as identifying when a developer leaves a “no-op” in code while planning future work. The speaker confirmed that AdaCore uses an internal AI reviewer to review merge requests.
Repository Maintenance and Toolchains: The speaker initiated a discussion on the status of Alier repositories, noting that some do not build, and they intend to perform maintenance. A participant asked about the possibility of using Alier to install special toolchains, and the speaker suggested continuing that conversation on the forum.
Ada 83 Compiler Project: A participant mentioned that a project has built an Ada 83 compiler using AI. While the implementation is written in C, the project is notable for successfully passing all AATS tests, serving as an interesting example of what can be accomplished with AI-driven development.
Conference Advocacy: The speaker discussed the goal of having more practitioners present on their experiences with Ada and Spark at industry conferences. They stated that funding is available to support travel and accommodations for speakers who wish to present, and encouraged participants to reach out if they have relevant content to share.
Documentation and Usability Feedback: A participant provided feedback on the Alier ecosystem, noting that while they frequently use the repositories, the documentation is often sparse compared to other ecosystems like Go. The participant suggested that requiring better documentation and examples as part of contribution standards would significantly improve usability. Other participants supported this, suggesting that a proposal be written on the forum comparing their experiences with Go and Alier to initiate improvement.
Embedded Design Standards: A participant raised concerns about embedded development, arguing that the current hardware abstraction layer (HAL) crates are not fully suitable for Spark due to their heavy use of object-oriented design. They suggested creating stricter standards for embedded systems design, especially for low-powered systems using a light runtime, and noted that they had posted proposals on the forum.
Automated Quality Checking: A participant asked if AI agents could be used to review repositories for documentation or compilation issues. The speaker confirmed this is possible and noted that they had already used an agent to download and attempt to build approximately 700 crates. They plan to use this data to identify which crates need documentation or updates, potentially submitting improvements to authors.
Hardware Abstraction Layer Portability: A participant discussed the challenges of writing generic drivers in Spark, noting that while generics help, they cannot easily have global contracts because dependencies vary by implementation. They suggested that cutting off at the HAL layer allows for better portability without constantly changing contracts, an area that remains open for further experimentation.
Zephyr RTOS Integration: The speaker discussed the use of the Zephyr RTOS with Ada, noting its performance, configurability, and support for various protocols like TCP/IP and MQTT. They explained that generating thin shim layers via AI allows for effective use of Zephyr’s device support in Ada code. A participant inquired about the complexity of Zephyr, and the speaker acknowledged the learning curve but noted that once configured, it provides a powerful, standardized platform.
Curated Indices for Embedded Crates: Participants discussed the possibility of creating a curated index or landing page for embedded Ada crates to improve visibility and compatibility. While they acknowledged the difficulty of maintaining such a list due to target-specific dependencies, they agreed that better documentation, grouping, or forum-based indexing could solve some of the discovery issues users currently face.
Meeting Closing: The speaker thanked all participants for their feedback and contributions. They committed to following up on the discussed topics, including reviewing the forum posts and scheduling the next meeting for two weeks later.