AdaCore/spark2014
View on GitHub ↗ ★ 332 Ada
SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
14 mentions on Hacker News by 11 people: 0 stories, 14 comments · first 2017-08-24 · latest 2025-11-01
20082026
-
…it require membership of some organization before you're allowed to view it? edit: did you mean https://github.com/AdaCore/spark2014 ?
comment by tremon · 2025-11-01 · in Open-Source Ada: From Gateware to Application -
SPARK tools are also open source. The main tool `gnatprove` is based on GCC as well. https://github.com/AdaCore/spark2014 It's not a community project, AFAICT. Few people know how to build it from source.
comment by i-con · 2025-11-01 · in Open-Source Ada: From Gateware to Application -
…with both GNAT FSF and GNAT PRO. The formal verification tool for SPARK, GNATprove, is open source. https://github.com/AdaCore/spark2014 Have a great day. :) Edit: I’m not affiliated with AdaCore. I’ve never even spoken to one of their…
comment by 0dyl · 2025-10-13 · in C++ Reflection and Qt MOC -
SPARK (Ada) is about as memory-safe as it gets. https://github.com/AdaCore/spark2014
comment by tiffanyh · 2025-04-27 · in Ask HN: Memory-safe low level languages? -
…Here's some other sorting algorithms proven with SPARK, with much more straightforward proofs: https://github.com/AdaCore/spark2014/blob/master/testsuite/g...
comment by LiamPowell · 2025-02-24 · in Is this the simplest (and most surprising) sorting algorithm ever? (2021) -
…(nada) https://docs.adacore.com/spark2014-docs/html/ug/search.html?... (nada) https://github.com/AdaCore/spark2014/issues?q=wavefront%20 (nada)
comment by SkyMarshal · 2025-02-14 · in Nvidia Security Team: “What if we just stopped using C?” (2022) -
…wish there was more active development on SPARK. It's largely untouched over the last 10-years. https://github.com/AdaCore/spark2014 For those not aware, SPARK gives even more safeguards/guarantees than Rust (see below) ... and also does…
comment by alberth · 2025-02-14 · in Nvidia Security Team: “What if we just stopped using C?” (2022) -
…various automatic theorem provers. Some examples of fully proven sorting functions are here: https://github.com/AdaCore/spark2014/blob/master/testsuite/g... You can also see from the above code just how good theorem provers and SPARK are…
comment by LiamPowell · 2024-12-28 · in Ada's dependent types, and its types as a whole -
…Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com/AdaCore/spark2014
comment by xentropy · 2020-09-04 · in Introduction to Ada -
…is on page 59 of PDF) See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/g...
comment by MaxBarraclough · 2020-04-28 · in Formal Verification Creates Hacker-Proof Code (2016) -
…https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [4]…
comment by MaxBarraclough · 2020-02-05 · in ZZ is a modern formally provable dialect of C -
Links for the lazy: https://ziglang.org https://github.com/AdaCore/spark2014
comment by SkyMarshal · 2019-07-19 · in We Need a Safer Systems Programming Language -
For the curious, there is an example Spark2014 tcp/ip stack at https://github.com/AdaCore/spark2014/blob/master/testsuite/g... (see README). Not clear how much of it they proved and at which level... And the README says it's not…
comment by touisteur · 2019-06-21 · in Smoltcp: A small TCP/IP stack in Rust -
Github, https://github.com/AdaCore/spark2014
comment by brudgers · 2017-08-24 · in About SPARK 2014