Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure. Learn more →
Spark2014 Alternatives
Similar projects and alternatives to spark2014
-
-
Stream
Stream - Scalable APIs for Chat, Feeds, Moderation, & Video. Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.
-
-
-
-
cuda-api-wrappers
Thin C++-flavored header-only wrappers for core CUDA APIs: Runtime, Driver, NVRTC, NVTX.
-
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
-
-
-
-
RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a better spark2014 alternative or higher similarity.
spark2014 discussion
spark2014 reviews and mentions
Posts with mentions or reviews of spark2014.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2025-02-13.
-
Is this the simplest (and most surprising) sorting algorithm ever? (2021)
See also: https://news.ycombinator.com/item?id=31975507
Here's some other sorting algorithms proven with SPARK, with much more straightforward proofs: https://github.com/AdaCore/spark2014/blob/master/testsuite/g...
- Nvidia Security Team: "What if we just stopped using C?" (2022)
-
Ada's Dependent Types, and Its Types as a Whole
> An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count!
It actually can be done in Ada, but not purely with the type system, instead we rely on SPARK, which converts Ada code and passes it through 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 now with the reasonably low number of assertions required to both prove that the output is sorted and prove that the input and output contain the same elements, not to mention all the hidden proofs relating to integer overflow, out-of-bounds access, etc..
-
NVIDIA Security Team: "What if we just stopped using C?" (This is not about Rust)
SPARK is available as open source and can be installed using Alire.
-
Community edition and FSF
gnatprove is open source. The whole SPARK is Open Source. :) The only difference between SPARK Pro and SPARK community is CodePeer tool included into SPARK Pro. Anything other (gnatprove, all 3 provers) are Open Source. Also, SPARK isn't owned by FSF, but by AdaCore.
-
Summary after Four Months with Ada — Programming with Ada documentation
The SPARK tool set is on GitHub and is GPL (https://github.com/AdaCore/spark2014). Note: Even though the SPARK tool set is under GPL, it only analyzes code and does not affect the binaries you produce with the compiler. This means it's possible to create proprietary SPARK software using the FSF GNAT compiler.
-
Code quality for hobby projects
"Proving" the correctness of the source code with GNATprove (SPARK) - with FSF GNAT. And preferably on the pipeline - Continuous Proving :)
-
A note from our sponsor - Stream
getstream.io | 17 Jul 2025
Stats
Basic spark2014 repo stats
8
283
9.9
1 day ago
AdaCore/spark2014 is an open source project licensed under GNU General Public License v3.0 only which is an OSI approved license.
The primary programming language of spark2014 is Ada.
Sponsored
Stream - Scalable APIs for Chat, Feeds, Moderation, & Video.
Stream helps developers build engaging apps that scale to millions with performant and flexible Chat, Feeds, Moderation, and Video APIs and SDKs powered by a global edge network and enterprise-grade infrastructure.
getstream.io