# General **URL:** https://forum.ada-lang.io/c/general/4.md?page=1 [Latest](https://forum.ada-lang.io/latest.md) · [Categories](https://forum.ada-lang.io/categories.md) · [Tags](https://forum.ada-lang.io/tags.md) **Page:** 2 --- ## [SPARK is now in the vericoding benchmark - 25/26 with a 30B model on a desktop](https://forum.ada-lang.io/t/spark-is-now-in-the-vericoding-benchmark-25-26-with-a-30b-model-on-a-desktop/4697)
**Author:** [@Tonyg](https://forum.ada-lang.io/u/Tonyg)\ **Replies:** 4\ **Last updated:** [August 31, 2026, 12:38pm UTC](https://forum.ada-lang.io/t/spark-is-now-in-the-vericoding-benchmark-25-26-with-a-30b-model-on-a-desktop/4697 "2026-08-31T12:38:32Z")
The vericoding benchmark (spec in, prover-accepted code out) covers Lean, Dafny and Rust/Verus. It had no Ada or SPARK track, so I have added one: Add a SPARK / GNATprove language track - Pull Request #320 - Beneficial-A… --- ## [I wonder if Ada can beat C here?](https://forum.ada-lang.io/t/i-wonder-if-ada-can-beat-c-here/4696)
**Author:** [@kevlar700](https://forum.ada-lang.io/u/kevlar700)\ **Replies:** 1\ **Last updated:** [August 31, 2026, 7:14am UTC](https://forum.ada-lang.io/t/i-wonder-if-ada-can-beat-c-here/4696 "2026-08-31T07:14:47Z")
--- ## [How to spawn a variable number of tasks on startup for SPARK?](https://forum.ada-lang.io/t/how-to-spawn-a-variable-number-of-tasks-on-startup-for-spark/4694)
**Author:** [@ValorZard](https://forum.ada-lang.io/u/ValorZard)\ **Replies:** 10\ **Last updated:** [August 30, 2026, 6:09pm UTC](https://forum.ada-lang.io/t/how-to-spawn-a-variable-number-of-tasks-on-startup-for-spark/4694 "2026-08-30T18:09:37Z")
Hello! Messing around a bit more with Ada, but a problem I"m running into is spawning a variable number of tasks on startup (specifically aiming for a “thread per core”). For whatever reason, I can’t seem to figure out… --- ## [Creating ADA-CTS (Cryptographic Testing Suite)](https://forum.ada-lang.io/t/creating-ada-cts-cryptographic-testing-suite/4683)
**Author:** [@Avila](https://forum.ada-lang.io/u/Avila)\ **Replies:** 2\ **Last updated:** [August 30, 2026, 2:02am UTC](https://forum.ada-lang.io/t/creating-ada-cts-cryptographic-testing-suite/4683 "2026-08-30T02:02:57Z")
IDEA ORIGINAL EN MI IDIOMA NATIVO por ende bcrytpgenrandom y processprng, son seguros criptograficamente perooo al hacer la conversion con mod Como sabemos (BCRYPTGENRANDOM, PROCESSPRNG ETC) son PRNGs criptograficame… --- ## [Why doesn't Ada/SPARK have lifetimes?](https://forum.ada-lang.io/t/why-doesnt-ada-spark-have-lifetimes/4677)
**Author:** [@ValorZard](https://forum.ada-lang.io/u/ValorZard)\ **Replies:** 17\ **Last updated:** [August 29, 2026, 6:53pm UTC](https://forum.ada-lang.io/t/why-doesnt-ada-spark-have-lifetimes/4677 "2026-08-29T18:53:00Z")
Hope this doesn’t sound too dumb, but why doesn’t SPARK have explicit lifetimes like rust does? Does SPARK just assume what your lifetimes are and proves them for you? --- ## [How do you handle console IO and string manipulation in SPARK?](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692)
**Author:** [@ValorZard](https://forum.ada-lang.io/u/ValorZard)\ **Replies:** 14\ **Last updated:** [August 29, 2026, 5:17pm UTC](https://forum.ada-lang.io/t/how-do-you-handle-console-io-and-string-manipulation-in-spark/4692 "2026-08-29T17:17:58Z")
Hey yall! I’ve been doing some more stuff with Ada and spark, and my goal has been to write programs that can be 100% audited with SPARK. However one issue I run into is how to handle printing out text and getting text… --- ## [State of some things: AEiC video recordings, Ada Monthly Meetups, Advocacy and others](https://forum.ada-lang.io/t/state-of-some-things-aeic-video-recordings-ada-monthly-meetups-advocacy-and-others/4639)
**Author:** [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Replies:** 3\ **Last updated:** [August 26, 2026, 1:42pm UTC](https://forum.ada-lang.io/t/state-of-some-things-aeic-video-recordings-ada-monthly-meetups-advocacy-and-others/4639 "2026-08-26T13:42:11Z")
Dear all, I would like to provide some updates on a few matters that I am carrying out. Most of the updates are somewhat negative, but there is a silver lighting to it. Ada Monthly Meetup As most of you have noticed, i… --- ## [Exception behavior with errno](https://forum.ada-lang.io/t/exception-behavior-with-errno/4658)
**Author:** [@sbenitezb](https://forum.ada-lang.io/u/sbenitezb)\ **Replies:** 21\ **Last updated:** [August 26, 2026, 8:53am UTC](https://forum.ada-lang.io/t/exception-behavior-with-errno/4658 "2026-08-26T08:53:14Z")
Hello. Does anybody know the GNAT behavior during exception raise or catch with respect to errno global variable? I assume that it might call some C function that might set it and trash previous C function errno state? --- ## [The status of ASIS](https://forum.ada-lang.io/t/the-status-of-asis/4642)
**Author:** [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)\ **Replies:** 20\ **Last updated:** [August 26, 2026, 7:19am UTC](https://forum.ada-lang.io/t/the-status-of-asis/4642 "2026-08-26T07:19:33Z")
I must admit being ignorant about ASIS. So my questions are: What is the status of the standard? Are the template packages here the actual stand of? --- ## [Found a bug with GNATProve/Spark when using protected objects](https://forum.ada-lang.io/t/found-a-bug-with-gnatprove-spark-when-using-protected-objects/4669)
**Author:** [@ValorZard](https://forum.ada-lang.io/u/ValorZard)\ **Replies:** 4\ **Last updated:** [August 26, 2026, 7:12am UTC](https://forum.ada-lang.io/t/found-a-bug-with-gnatprove-spark-when-using-protected-objects/4669 "2026-08-26T07:12:38Z")
I was able to us AI to get a reproducible version of it, you can check it out here: GitHub - ValorZard/spark\_po\_pointer\_repro · GitHub full crash: PS C:\\ada-stuff\\spark\_po\_pointer\_repro\> alr exec -- gnatprove -P spark… --- ## [Alire with microbit v1](https://forum.ada-lang.io/t/alire-with-microbit-v1/4659)
**Author:** [@bjorn-lundin](https://forum.ada-lang.io/u/bjorn-lundin)\ **Replies:** 6\ **Last updated:** [August 24, 2026, 6:13pm UTC](https://forum.ada-lang.io/t/alire-with-microbit-v1/4659 "2026-08-24T18:13:49Z")
Hi, I’ve spent some (several) hours now to get a trivial example to link for a bbc:microbit card V1. Google AI was involved but it did not help that much. I’m on opensuse 16 and have no compiler installed. In the end… --- ## [Ada/SPARK, marketing, reach and the abysmal state of things](https://forum.ada-lang.io/t/ada-spark-marketing-reach-and-the-abysmal-state-of-things/4019)
**Author:** [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Replies:** 32\ **Last updated:** [August 23, 2026, 3:47pm UTC](https://forum.ada-lang.io/t/ada-spark-marketing-reach-and-the-abysmal-state-of-things/4019 "2026-08-23T15:47:33Z")
Hi all, I am watching some of the new videos uploaded to YT in the ACM SIGPLAN channel and it is just depressing. There are a ton of videos about formal proofs, better software quality, software analysis, etc; and SPARK… --- ## [Alire community index browser](https://forum.ada-lang.io/t/alire-community-index-browser/4653)
**Author:** [@yrashk](https://forum.ada-lang.io/u/yrashk)\ **Replies:** 6\ **Last updated:** [August 23, 2026, 5:03am UTC](https://forum.ada-lang.io/t/alire-community-index-browser/4653 "2026-08-23T05:03:11Z")
Hi everybody, As I was working on the web interface for Flyology’s Alire index, I realized I could easily extend it to the community index, too. Hopefully, you’ll find it useful: Alire Community Shadow It has a feed of… --- ## [SPARK, floting points and the Colibri solver](https://forum.ada-lang.io/t/spark-floting-points-and-the-colibri-solver/4631)
**Author:** [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Replies:** 7\ **Last updated:** [August 22, 2026, 9:52pm UTC](https://forum.ada-lang.io/t/spark-floting-points-and-the-colibri-solver/4631 "2026-08-22T21:52:05Z")
Dear all, I would like to share with you an experiment. Now that I am using AI for quite a few things I do not have time to do by hand, I got the idea to revisit the possibility of enabling the Colibri family of SMT sol… --- ## [Is the source to the Ada Reference Manual Formatting Tool available online anywhere more convenient](https://forum.ada-lang.io/t/is-the-source-to-the-ada-reference-manual-formatting-tool-available-online-anywhere-more-convenient/4648)
**Author:** [@TKurtBond](https://forum.ada-lang.io/u/TKurtBond)\ **Replies:** 2\ **Last updated:** [August 20, 2026, 1:35pm UTC](https://forum.ada-lang.io/t/is-the-source-to-the-ada-reference-manual-formatting-tool-available-online-anywhere-more-convenient/4648 "2026-08-20T13:35:03Z")
… than the CVSWeb interface? --- ## [I love SPARK Bronze mode as a baseline](https://forum.ada-lang.io/t/i-love-spark-bronze-mode-as-a-baseline/4641)
**Author:** [@kevlar700](https://forum.ada-lang.io/u/kevlar700)\ **Replies:** 0\ **Last updated:** [August 17, 2026, 11:37am UTC](https://forum.ada-lang.io/t/i-love-spark-bronze-mode-as-a-baseline/4641 "2026-08-17T11:37:19Z")
I just came here to say I had a multi loop with some thorny Status handling and I love that the following can be so helpful by itself. Gnat Studio =\> SPARK =\> Examine all sources =\> Do not report warnings =\> Analysis mo… --- ## [No\_Dependence restriction](https://forum.ada-lang.io/t/no-dependence-restriction/4636)
**Author:** [@cantanima](https://forum.ada-lang.io/u/cantanima)\ **Replies:** 2\ **Last updated:** [August 14, 2026, 7:24pm UTC](https://forum.ada-lang.io/t/no-dependence-restriction/4636 "2026-08-14T19:24:48Z")
I was reading Chapter 13 in the Barnes text on Ada 2022 and came across the No\_Dependence restriction. OK, why? I’m sure there’s a reason, but all I could think of is: package A depends on package B, for some reason A i… --- ## [Towards a HAL for multiple runtimes](https://forum.ada-lang.io/t/towards-a-hal-for-multiple-runtimes/4364)
**Author:** [@ThyMYthOS](https://forum.ada-lang.io/u/ThyMYthOS)\ **Replies:** 25\ **Last updated:** [August 14, 2026, 3:33pm UTC](https://forum.ada-lang.io/t/towards-a-hal-for-multiple-runtimes/4364 "2026-08-14T15:33:05Z")
We currently have Ada\_Drivers\_Library which targets ZFP runtimes or at least the drivers included often don’t use interrupts or any higher level tasking features. Also the interfaces are typically synchronous: The proced… --- ## [GCC bans AI contributions](https://forum.ada-lang.io/t/gcc-bans-ai-contributions/4617)
**Author:** [@dmitry-kazakov](https://forum.ada-lang.io/u/dmitry-kazakov)\ **Replies:** 10\ **Last updated:** [August 13, 2026, 9:18pm UTC](https://forum.ada-lang.io/t/gcc-bans-ai-contributions/4617 "2026-08-13T21:18:26Z")
I think it is relevant in the context of GNAT and simply worth to mention. Here is the link to the LWN.net article. --- ## [How to delete a file from a GitHub branch](https://forum.ada-lang.io/t/how-to-delete-a-file-from-a-github-branch/3800)
**Author:** [@Nordic\_Dogsledding](https://forum.ada-lang.io/u/Nordic_Dogsledding)\ **Replies:** 7\ **Last updated:** [August 13, 2026, 1:55pm UTC](https://forum.ada-lang.io/t/how-to-delete-a-file-from-a-github-branch/3800 "2026-08-13T13:55:04Z")
Docs say: Navigate to the repository and locate the file you want to delete. Click on the file to open it. Click the trash can icon (:wastebasket:) labeled “Delete this file” at the top right. There is no trash icon. … --- ## [NVIDIA looking for Ada SPARK programmers](https://forum.ada-lang.io/t/nvidia-looking-for-ada-spark-programmers/4630)
**Author:** [@markhermeling](https://forum.ada-lang.io/u/markhermeling)\ **Replies:** 0\ **Last updated:** [August 12, 2026, 6:22pm UTC](https://forum.ada-lang.io/t/nvidia-looking-for-ada-spark-programmers/4630 "2026-08-12T18:22:23Z")
This is a fantastic team, building ground breaking products that go into cars and physical AI: --- ## [Building a Pure Ada APK/DEX Reverse Engineering Tool](https://forum.ada-lang.io/t/building-a-pure-ada-apk-dex-reverse-engineering-tool/4626)
**Author:** [@ibousv](https://forum.ada-lang.io/u/ibousv)\ **Replies:** 2\ **Last updated:** [August 8, 2026, 5:40pm UTC](https://forum.ada-lang.io/t/building-a-pure-ada-apk-dex-reverse-engineering-tool/4626 "2026-08-08T17:40:27Z")
Hello Ada Community, I am a junior developer diving into Ada, and I believe the best way to master a language is by building something real and challenging. To learn Ada, system-level stream parsing, and formal verific… --- ## [Formally verified, bias-free entropy conversion engine in Ada/SPARK](https://forum.ada-lang.io/t/formally-verified-bias-free-entropy-conversion-engine-in-ada-spark/4608)
**Author:** [@Avila](https://forum.ada-lang.io/u/Avila)\ **Replies:** 9\ **Last updated:** [August 7, 2026, 2:30am UTC](https://forum.ada-lang.io/t/formally-verified-bias-free-entropy-conversion-engine-in-ada-spark/4608 "2026-08-07T02:30:10Z")
Hi everyone, Quick note: English is my second language, so I am using an AI to help translate this into proper technical English, as Spanish is my native tongue. I wanted to share a complete architecture designed in Ad… --- ## [Larger Corpus of SPARK (preferably pre-2014) code?](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614)
**Author:** [@lojikil](https://forum.ada-lang.io/u/lojikil)\ **Replies:** 6\ **Last updated:** [August 7, 2026, 1:57am UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614 "2026-08-07T01:57:53Z")
I’m looking for larger examples of SPARK code, esp pre-SPARK 2014. It’s easier to find examples of older Ada code bases, and new SPARK code, but I’d like to see larger and more complete examples of older SPARK code. Does… --- ## [New job postings for Ada in the railway sector](https://forum.ada-lang.io/t/new-job-postings-for-ada-in-the-railway-sector/4605)
**Author:** [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Replies:** 1\ **Last updated:** [August 4, 2026, 3:32am UTC](https://forum.ada-lang.io/t/new-job-postings-for-ada-in-the-railway-sector/4605 "2026-08-04T03:32:43Z")
As most of you will already know, Ada is used quite a bit in France for many purposes, including Railway. Hitachi has two open positions both listing Ada as a language: https://careers.hitachi.com/jobs/17954080-ingenieu… --- ## [Weird error: nonoverridable aspect "String\_Literal"](https://forum.ada-lang.io/t/weird-error-nonoverridable-aspect-string-literal/4603)
**Author:** [@Blady](https://forum.ada-lang.io/u/Blady)\ **Replies:** 6\ **Last updated:** [August 2, 2026, 7:47am UTC](https://forum.ada-lang.io/t/weird-error-nonoverridable-aspect-string-literal/4603 "2026-08-02T07:47:42Z")
Consider this code: (from AARM 4.2.1 User-Defined Literals) 13. Max\_Roman\_Number : constant := 3\_999; -- MMMCMXCIX 14. 15. type Roman\_Number is range 1 .. Max\_Roman\_Number 16. with String\_Literal =\> To\_Rom… --- ## [Any problems using "extends" in a gpr file used with Alire?](https://forum.ada-lang.io/t/any-problems-using-extends-in-a-gpr-file-used-with-alire/4599)
**Author:** [@pat-rogers](https://forum.ada-lang.io/u/pat-rogers)\ **Replies:** 2\ **Last updated:** [July 30, 2026, 3:31pm UTC](https://forum.ada-lang.io/t/any-problems-using-extends-in-a-gpr-file-used-with-alire/4599 "2026-07-30T15:31:10Z")
I have a new crate that doesn’t implement two package bodies because clients are meant to do so. But because Alire won’t publish a crate that won’t compile everything successfully (IIUC), my crate provides dummy bodies (… --- ## [How did you start with AI helping to code?](https://forum.ada-lang.io/t/how-did-you-start-with-ai-helping-to-code/4592)
**Author:** [@bjorn-lundin](https://forum.ada-lang.io/u/bjorn-lundin)\ **Replies:** 11\ **Last updated:** [July 30, 2026, 11:03am UTC](https://forum.ada-lang.io/t/how-did-you-start-with-ai-helping-to-code/4592 "2026-07-30T11:03:25Z")
I just watched https://www.youtube.com/watch?v=L2ExrasTGx8 and it was very interesting. I use GPS daily, and I wonder if anyone has set it up to use AI-tools with it (and if it is possible at all) Or should I migrate t… --- ## [In Alire, how to use SPARKlib without all assertions enabled?](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595)
**Author:** [@pat-rogers](https://forum.ada-lang.io/u/pat-rogers)\ **Replies:** 5\ **Last updated:** [July 29, 2026, 12:09pm UTC](https://forum.ada-lang.io/t/in-alire-how-to-use-sparklib-without-all-assertions-enabled/4595 "2026-07-29T12:09:16Z")
I have recently published my first crate (Proven\_Components) that contains a bunch of reusable packages that I’ve written over the years and updated as Ada evolved. Most are now formally proven. Proof for one of them (s… --- ## [Controlling elaboration order when Ada.Real\_Time package is used](https://forum.ada-lang.io/t/controlling-elaboration-order-when-ada-real-time-package-is-used/4593)
**Author:** [@BottCode](https://forum.ada-lang.io/u/BottCode)\ **Replies:** 6\ **Last updated:** [July 28, 2026, 8:31am UTC](https://forum.ada-lang.io/t/controlling-elaboration-order-when-ada-real-time-package-is-used/4593 "2026-07-28T08:31:24Z")
I was reading the Guide for the use of the Ada Ravenscar Profile in high integrity systems, in particular the specification of Activation\_Manager package at page 67. with Ada.Real\_Time; package Activation\_Manager is … [Previous page](https://forum.ada-lang.io/c/general/4.md) [Next page](https://forum.ada-lang.io/c/general/4.md?page=2)