mizchi/dspec

This project is an early prototype of a system for writing software specifications that a computer can actually check and run, instead of specifications that are just plain text documents nobody verifies. It uses a typed configuration language called Pkl to author the specification, so mistakes in the spec's structure get caught early, before that spec is compared against real code or real behavior. The core idea is that a spec written in Pkl has a stable schema and unique ids for each piece, and from that structured spec the tool can generate a natural language description in different languages, check whether a real application matches what the spec describes, and detect drift when the spec and the implementation fall out of sync over time. The command line tool included in the project offers a very large number of operations: checking a spec file for consistency, rendering it as readable text, comparing two versions of a spec to see if a change is backward compatible or breaking, importing facts from a real running application to compare against the spec, and generating structured reports and coverage numbers about how much of a spec has been verified. For deeper formal verification, the project can hook into established tools from computer science research, including TLA+, Alloy, Z3, and Lean, which are used to mathematically prove properties about a system rather than just testing it. This is an early, experimental prototype rather than a finished product, and it currently requires the Nix package manager to set up its development environment with all the required tools installed together. It is aimed at developers and researchers who work on specification-driven or formally verified software, not general audiences. The full README is longer than what was shown.