# Some proved SPARK helpers
**URL:** https://forum.ada-lang.io/t/some-proved-spark-helpers/4738
**Category:** General
**Tags:** spark
**Created:** [September 14, 2026, 12:25am UTC](https://forum.ada-lang.io/t/some-proved-spark-helpers/4738 "2026-09-14T00:25:19Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@ksson](https://forum.ada-lang.io/u/ksson)
#### Post date: [September 14, 2026, 12:25am UTC](https://forum.ada-lang.io/t/some-proved-spark-helpers/4738/1 "2026-09-14T00:25:19Z")
Hello,
Coding agents have seen very good progress with SPARK proofs in particular, so I wondered if it was possible to develop proved every-day tools in them. Here are three I tried recently:
- fully proved SPARK fuzzy matcher, with fzf-like integration for bash history search and file search (ctrl-R and ctrl-T): [GitHub - kanigsson/fuzzy: A fuzzy matcher library in SPARK · GitHub](https://github.com/kanigsson/fuzzy)
- fully proved SPARK regex engine, with grep and rg-like CLI wrappers: [GitHub - kanigsson/spark\_re · GitHub](https://github.com/kanigsson/spark_re)
- proved SPARK differ and apply function (plus proof that apply of the obtained diff yields the target content), with diff-wrapper (but not patch): [GitHub - kanigsson/spark\_diff · GitHub](https://github.com/kanigsson/spark_diff)
I have started to use those tools in my daily workflow. Some notes:
- What is proved exactly still needs qualification, and is qualified in each repo, but for the most part these can be considered platinum proofs;
- But SPARK doesn’t cover everything, in particular stack overflow or other resource exhaustion can still happen;
- The CLI wrappers are not proved;
- The tools pale in terms of efficiency compared to the real-world tools. But still usable (well, maybe spark-rg is quite slow …).
All of the above are fully generated by coding agents, with some small manual modifications (e.g. README). So there is a lot of AI prose, sorry.
I plan to continue working on these, especially for efficiency. If you are want to see improvements, let me know and I will try to implement them. Or you can just make your own, better version, I would like to see those as well.
Disclaimer: I am an AdaCore employee but these are not AdaCore products or otherwise endorsed by the company.
---
### Author:  [@docandrew](https://forum.ada-lang.io/u/docandrew)
#### Post date: [September 14, 2026, 11:44pm UTC](https://forum.ada-lang.io/t/some-proved-spark-helpers/4738/2 "2026-09-14T23:44:53Z")
Really cool! Will definitely be watching these, I might have a need for them in the near future.