Very interesting set of topics that flew by, summary below and video will be attached shortly. Thanks for everybody that joined! I am going to try and see if I can arrange for a SPARK hands-on-walkthrough in one of the next sessions.
Summary
Technical demonstrations and community initiatives underscored advances in formal verification and Ada ecosystem developments via AI integration.
Proof Systems and Education
Participants examined strategies for managing proof assertions and state space complexities while launching new educational resources. Developers confirmed that AI tools significantly lower the barrier to entry for formal verification.
Ada Ecosystem and Projects
The community launched a proposal system to fund tasks ranging from runtime improvements to new parallel features. These initiatives prioritize real-world challenges and hardware testing environments.
WebAssembly and AI Strategy
Demonstrations showcased running verified Ada code within browsers using WebAssembly. Teams adopted a cost-effective tiered strategy for using AI models to maximize idiomatic code generation.
Details
-
Proof Assertions and State Space: Daniel King explains that incorporating intermediate assertions into proofs helps bridge gaps and guide the prover by validating assumptions at specific points, though this can increase the proof context. To manage this, Daniel King suggests breaking problems down into smaller procedures or using ghost code—procedures with a precondition and a postcondition—to reduce the amount of information the prover must search through. William Harvey notes that for those with significant experience, acquiring the tacit knowledge required for these tools is challenging and suggest that video tutorials or recorded proof sessions to demonstrate how to navigate proof states would be nice .
-
Learning Resources for Proof Systems: Mark Hermeling addresses the need for learning content, noting that Olivier is thinkint of launching a Twitch channel to walk through problem-solving in real-time. Additionally, Mark Hermeling highlights two recent resources: a blog post by Tony Ayello detailing gold proof work on the Mars rover and recent posts by Claire Dross regarding complex proofs, which are recommended for further study.
-
Ada User Awards and Project Proposals: Fernando Oleo provides an overview of the Ada user awards initiative, which aims to incentivize community development in the Ada ecosystem. With feedback from the community and donations, five proposals have been created, including tasks for creating a compiler-independent sockets library and documenting the implementation of GNAT runtime systems, all of which include financial rewards .
-
Parallel Features and Sephur Runtime: Fernando Oleo describes additional proposal tasks, such as creating examples and benchmarks for new parallel features in Ada 2022 and developing an official or community-standard Sephur RTOS runtime system. He confirms that AI can be used for this development provided it is disclosed and the work remains human-driven .
-
WebAssembly for High-Performance Applications: Fernando Oleo explains that WebAssembly allows high-performance, native-like applications to run in browsers and on small microchips . WebAssembly operates in a restricted, guarded environment, effectively acting like a small virtual machine or a separation kernel, which provides security benefits for rapid deployment .
-
Hack Compiler Demonstration: Fernando Oleo showcases work done by Aldo, who used the GNAT LLVM compiler to compile the Hack compiler into WebAssembly. This allows the compiler to run directly within a browser without server-side networking . Aldo modified the compiler to improve exception handling and expanded the WebAssembly runtime to support features like file reading and streams .
-
Spark Verification in WebAssembly: Fernando Oleo highlights the potential for running Spark-verified Ada code in browsers or IoT devices via WebAssembly. This approach enables the benefits of formal verification, typically reserved for safety-critical systems, to be utilized in more common, edge-based applications. Furthermore, the WebAssembly standard itself is mathematically verified, ensuring correct code generation properties .
-
Technical Architecture of Hack and WebAssembly: Niklas Holsti and Fernando Oleo discuss the architecture, clarifying that in the current demonstration, the WebAssembly interpreter is interpreting the Hack interpreter, which in turn interprets the Hack intermediate code . While native compilation of Hack to WebAssembly remains a topic for future exploration, Fernando Oleo notes that some developers have already successfully compiled LLVM to WebAssembly to create full compiler infrastructures .
-
Runtime Systems and WASI: Fernando Oleo elaborates on runtime system improvements, noting that Aldo has added support for timing and calendar functionality, with ongoing work regarding tasking and file input/output. Aldo is utilizing the WebAssembly System Interface (WASI) to handle external interactions, such as file access, within the WebAssembly environment .
-
Community-Driven Development Flow: Mark Hermeling and Fernando Oleo explain that the project proposal process is community-driven, where members identify needs—such as the request for GNAT LLVM integration in Alire—and propose tasks for financial rewards. This allows the community to prioritize documentation, runtime improvements, and new features based on real-world challenges, such as the reverse engineering of specific hardware .
-
Recent Conference Insights and NVIDIA Usage: Mark Hermeling reports on findings from the ASEE and SDV USA conferences. He highlights that NVIDIA utilizes Ada and Spark for bootloaders and Drive OS kernels on their platforms, which include approximately 30 ARM cores and various AI accelerators . This adoption of formal methods has led to a significant reduction in bugs—such as memory safety issues—compared to equivalent C++ implementations .
-
AI-Assisted Contract Writing: Mark Hermeling discusses the role of AI in lowering the barrier to using formal methods. He notes that while writing Spark contracts can be difficult, AI tools significantly simplify the process, effectively removing the “blindfold” when working with formal proofs .
-
Translating Legacy Code to Spark: Mark Hermeling details successful experiments using frontier AI models to translate C code into Ada and subsequently lift it to Spark. By using these models, they successfully translated components like Linux kernel GPIO drivers and parts of curl, emphasizing the models’ capability to generate the necessary C-shim layers to map types and handle macro-heavy code.
-
Ada Language Proposal Process: Étienne Coulouma inquires about a formal proposal process similar to Python’s Enhancement Proposals. Fernando Oleo explains that proposals can be submitted to the Ada Rapporteur Group (ARG) or handled through compiler extensions, noting that GNAT extensions, such as pattern matching on case statements, were successfully implemented via this approach .
-
Hardware Testing Environments: Mark Hermeling describes current efforts to set up automated testing for Ada runtime systems. He is using Renode for device emulation and is working on configuring physical hardware testing using ST micro boards and the Raspberry Pi Pico 2 with hardware debuggers.
-
Strategies for Cost-Effective AI Usage: Fernando Oleo and Mark Hermeling discuss the economic side of using AI for development Fernando Oleo shares a strategy of using cheaper, faster models (such as DeepSeek V4) for drafting code, and reserving more expensive models for the final review and polish, which maximizes productivity while remaining cost-efficient.
-
AI Model Capabilities and Idiomatic Code: Fernando Oleo notes that after providing a corpus of instructions and examples, cheaper models are capable of writing fairly idiomatic Spark code. While these models may occasionally struggle with complex tasks like subtype and set theory implementation, they can be corrected with simple prompts, and their performance continues to improve .