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
- fully proved SPARK regex engine, with grep and rg-like CLI wrappers: GitHub - kanigsson/spark_re · GitHub
- 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
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.