# Larger Corpus of SPARK (preferably pre-2014) code?
**URL:** https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614
**Category:** General
**Tags:** spark
**Created:** [August 5, 2026, 11:05pm UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614 "2026-08-05T23:05:20Z")
**Posts on this page:** 7
**Page:** 1
### Author:  [@lojikil](https://forum.ada-lang.io/u/lojikil)
#### Post date: [August 5, 2026, 11:05pm UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/1 "2026-08-05T23:05:20Z")
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 anyone know some?
---
### Author:  [@OneWingedShark](https://forum.ada-lang.io/u/OneWingedShark)
#### Post date: [August 6, 2026, 12:49am UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/2 "2026-08-06T00:49:29Z")
I think most are going to be SPARK 2014; prior to this version of SPARK, this language used annotated comments for proving.
There’s a large project “Tokeneer” that was done all in SPARK, I think by the NSA and made available.
---
### Author:  [@lojikil](https://forum.ada-lang.io/u/lojikil)
#### Post date: [August 6, 2026, 1:19am UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/3 "2026-08-06T01:19:22Z")
That example is great, thank you! I actually have John Barnes’ _High Integrity Software: The SPARK Approach to Safety and Security_, which had me thinking about older SPARK codebases. It seems like there aren’t many complete examples out there, but I’ll look around for Tokeneer.
---
### Author:  [@OneWingedShark](https://forum.ada-lang.io/u/OneWingedShark)
#### Post date: [August 6, 2026, 3:16am UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/4 "2026-08-06T03:16:03Z")
Original SPARK 2005: [GitHub - martin-cs/Tokeneer · GitHub](https://github.com/martin-cs/Tokeneer)
The updated SPARK 2014 code: [spark2014/testsuite/gnatprove/tests/tokeneer at master · AdaCore/spark2014 · GitHub](https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/tokeneer)
---
### Author:  [@lojikil](https://forum.ada-lang.io/u/lojikil)
#### Post date: [August 6, 2026, 1:17pm UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/5 "2026-08-06T13:17:18Z")
Thank you! I found those after you mentioned Tokeneer, as well as some wayback machine references to the original AdaCore site (I wish they didn’t kill old webpages as frequently as they seem to do…). It also looks like the “Ada Gems” papers have some interesting commentary on Tokeneer and other SPARK code bases, so I might try to build some references around it. Thank you again for this!
---
### Author:  [@OneWingedShark](https://forum.ada-lang.io/u/OneWingedShark)
#### Post date: [August 6, 2026, 5:25pm UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/6 "2026-08-06T17:25:14Z")
You’re welcome.
I hope it helps.
BTW, what is your interest in the older varient?
SPARK 2014 using Ada 2012’s aspect system was an incredible leap forward: having the proof’s definitions be legitimate code for the host language eliminates the “annotations got out of sync” problem, and it encourages the proof-system to be integrated into the compiler. (Though it is separate with GNAT, I can easily imagine a compiler integrated with static analysis and proof engines.)
---
### Author:  [@lojikil](https://forum.ada-lang.io/u/lojikil)
#### Post date: [August 7, 2026, 1:57am UTC](https://forum.ada-lang.io/t/larger-corpus-of-spark-preferably-pre-2014-code/4614/7 "2026-08-07T01:57:53Z")
I’ve been on a bit of an Ada book bender, and SPARK seems extremely interesting, but I couldn’t find as much about older SPARK versions outside of literature. So mainly historical curiosity combined with with an interest in the semantics of the language and how it would manifest in an actual codebase.