This work-in-progress tool validates assertions involving finite-dimensional linear algebra on a best-effort basis using a combination of SMT solving and searching for counterexamples.

For design docs, see docs/.

For input/output examples, see tests/fixtures. For example, tests/fixtures/validate_arguments_input.md is an input to this system with tests/fixtures/validate_arguments_output.md as a corresponding output.