Hi @nbjessen,
welcome to the forums!
As Luke said, SPARK is probably what you are looking for. It is a formal verification language/system for Ada. Think of testing, but on steroids, fully automatic, fully exhaustive, fully mathematical and fully documented. Basically, you encode (program) your software in Ada, annotate it (with code), which also doubles as documentation, and then have SPARK/GNATprove take over and let it check whether those annotations are actually fulfilled. It is used in safety critical systems. The more recent news is NVIDIA’s DriveOS (7 million line OS) was certified to SIL-4 as per ISO26262. If you would like some quick introductions to SPARK, look into:
- Long presentation about SPARK FOSDEM 2018 - SPARK Language: Historical Perspective & FOSS Development (a lot of the info about the limitations is now outdated)
- Short and sweet presentation about SPARK and how to get started: FOSDEM 2023 - Get Started with Open Source Formal Verification
- (Disclaimer, my own presentation) about how to create richer and verifiable software with liquid types and contracts in SPARK: FOSDEM 2025 - Understanding liquid types, contracts and formal verification with Ada/SPARK
I do agree that verified Ada could be the future of “the full stack” from HW definition to final application. Currently, there is no Ada → HDL compiler… HOWEVER, there are C → HDL compilers and there is an Ada → C compiler. So one can do (verified) Ada → C → HDL. The Ada → C compiler is GNAT-LLVM with its CCG backend. It does not currently compile all Ada features (mainly exceptions) but generally, these features should not be used in HDL.
Also, regarding having a full open stack for HW design all the way to final applications… It already exists!!! We have a fully open source ecosystem (SystemVerilog, VHDL, verifiers, synth, routing, etc, etc), which you can find precompiled and documented here: GitHub - YosysHQ/oss-cad-suite-build: Multi-platform nightly builds of open source digital design and verification tools
Additionally, there are tools/frameworks such as Litex GitHub - enjoy-digital/litex: Build your hardware, easily! which abstract all this complexity away and allows for the automated creation of SVD files. These can be easily transformed into Ada code for a HAL (Hardware Abstraction Layer).
Finally, all of this can be tested in software with the use of simulators (again, see the oss-cad-suite link) or with a full “emulated” board with the use of Renode.
The actual implementation of what I have written here can be found in greater detail in these two blog-posts as written by @ohenley:
- Open-Source Ada: From Gateware to Application | The AdaCore Blog
- Getting Started with Renode: Simulating an Ada… | The AdaCore Blog
Basically, I am of the opinion that we are much closer to your idea than you may want to believe!
Also, we do have fully verified standard libraries, such as GitHub - AdaCore/SPARKlib and fully verified OS such as GitHub - jgrivera67/HiRTOS: HiRTOS: a high-integrity multi-core RTOS kernel and separation kernel written in SPARK Ada, https://muen.codelabs.ch/ and a larger UNIX one (partially verified and built by a couple of young adults in their 20s) https://ironclad-os.org/ For low level stuff we have the amazing GitHub - gabriele-galeotti/SweetAda: Ada-language framework and GitHub - AdaCore/bb-runtimes: Source repository for the GNAT Bare Metal BSPs
Best regards,
Fer