speccheck — Ensure software integrity with comprehensive…

Pitch

Description

Comments

About this project

speccheck provides a robust solution for verifying software against declared specifications. By analyzing a SPEC.md alongside code and test results, it delivers precise evidence-backed statuses for each requirement. This tool not only enhances confidence in software quality but also embodies the principles of specification engineering for reliable software development.

speccheck is a sophisticated Specification Conformance Checker designed to ensure that software meets its specified requirements. By analyzing a SPEC.md file that outlines various system specifications, speccheck works seamlessly with the associated codebase and its tests to determine compliance. The tool provides a clear, evidence-backed status for each requirement, contract, invariant, constraint, edge case, and acceptance test defined in the specification.

Key Features

Evidence Generation: For each declaration in the SPEC.md, speccheck identifies relevant code and test citations, generating reports that unambiguously demonstrate compliance based solely on factual citations and JUnit results. The output remains consistent across multiple runs with identical inputs, ensuring reliability.
Optional Model-Backed Judge: In addition to standard checking, an optional AI-driven judge can evaluate passing tests to provide a downgrade verdict if sufficient assertions are not made, adding an extra layer of scrutiny to the verification process.

Workflows Supported by speccheck

The workflow facilitated by speccheck emphasizes the significance of written specifications as the ultimate source of truth over casual conversations. This approach ensures:

Clarity and Precision: With clearly defined obligations and traceable IDs, both human developers and automated systems can measure compliance without ambiguity.
Automation: The automated nature of the tool minimizes human error, shifting the evaluative burden from reviewers to verifiable evidence derived directly from the specifications.

SPEC.md Structure

The SPEC.md file follows a defined structure for optimal processing:

Section	Description
Front Matter	Contains status, version, and other metadata
§0 Intent	Purpose and boundaries of the system
§1 Actors	Identifies actors involved in system behavior
§2 Requirements	Specific obligations formatted in normative language
§3 Behavior and State	Lifecycle and main flow
§4 Contracts	Definitions of significant interfaces
§5 Interfaces	Actual surfaces for interaction
§6 Invariants	Must-have properties of implementations
§7 Constraints	Measurable limits placed on system behavior
§8 Edge Cases	Specifications for boundary behavior
§9 Tests	Unambiguous acceptance tests
§10 Dependencies	Necessary runtime and library details
§11 Traceability	Links between requirements, contracts, and tests
§12 Decisions	Documented rationale for decisions made

Skills and Modules

Accompanying the main checker are several specialized skills that enhance the specification engineering process:

Skill	Purpose	Output
spec-proposal	Propose changes to existing specifications	Proposal documents
spec-writing	Craft and update specifications	Updated SPEC.md
spec-review	Audit specifications for rigor	Review Reports
spec-plan	Create implementation plans	Implementation plans
spec-build	Execute specification building and testing	Implementation output
spec-model	Model specifications for gaps analysis	Model findings
spec-proof	Verify implementation against specifications	Proof documentation

Usage

speccheck provides a user-friendly command-line interface to run checks efficiently:

speccheck check --spec SPEC.md --src src --tests tests --results junit.xml --judge mock --out reports

This initiates a spectrum of verifications that include analyzing specified requirements against actual code tests to produce conformance reports, detailing passing, skipping, failing, and unverified statuses. Each run produces a comprehensive summary to aid developers in ensuring software quality.

In conclusion, speccheck serves as an invaluable tool that transforms the specification process from a subjective assertion to a verifiable, evidence-based practice, bringing efficiency and accountability to software development.