covex

Zero-dependency Ada/SPARK CLI tool for coverage analysis, proof verification, test-result parsing, DO-178C DAL compliance assessment, and interactive dashboards.

• Source scanning: walks .ads files, extracts subprogram declarations, docstring annotations (@param, @return, @field, @formal), and HLR traceability tags
• Proof analysis: parses GNATprove gnatprove.out summaries; assesses SPARK assurance levels (Stone through Platinum)
• Test parsing: reads markdown test results for pass/fail counts (native Ada or AUnit format)
• DAL compliance: assesses DO-178C DAL A-E criteria (HLR coverage, orphan tags, test status, minimum SPARK proof level)
• Multiple outputs: ANSI terminal report, SVG badges, Markdown reports, HTML dashboard, and JSON API via built-in HTTP/1.1 server
• Scalable: package/subprogram collections use Ada.Containers.Vectors (heap-allocated, no compile-time limits)
• No external dependencies beyond the GNAT runtime library
• Self-assessment: 100% docstring coverage, Platinum SPARK (28/28 VCs proved), DAL-C Achieved, 152/152 native tests passing