MatCli

A Lean 4 package for mechanically verifying closed, finite rule systems.

MatCli exhaustively checks a declared universe of facts, actions, rules, fact exclusions, incompatibilities, and infeasibility conditions. Its pure verifier returns one typed report, while an optional adapter loads JSON artifacts and emits stable human-readable or JSON output.

Table of Contents

• Install
• Usage
  • Library
  • CLI
• Verification Contract
• Reports and Evidence
• Documentation
• API
• Contributing
• License

Install

Install Lean with elan, then clone and build the repository:

git clone https://github.com/jackyang25/matcli.git
cd matcli
lake build

The repository pins Lean 4.15.0 in lean-toolchain and depends only on Lean's standard library.

Usage

Library

Import MatCli, construct a Verification.Bundle, and run the pure verifier:

import MatCli

open MatCli.Verification

variable {Fact Action : Type}
  [DecidableEq Fact] [DecidableEq Action]

def verifyBundle (bundle : Bundle Fact Action) : Report Fact Action :=
  verify bundle

Import MatCli.Artifacts only when loading JSON artifacts or producing an integration report:

import MatCli.Artifacts

open MatCli.Artifacts

def verifyArtifacts (paths : Paths) : IO (Except LoadError Lean.Json) := do
  match <- loadBundle paths with
  | .error error => pure (.error error)
  | .ok loaded => pure (.ok (reportToJson (verifyLoaded loaded)))

Expected read, JSON, schema-version, and value-conversion failures are returned as typed LoadError values. Artifact schema 1.0 is enforced.

CLI

Run the bundled example:

lake env lean --run VerifyMain.lean -- --example

Verify external artifacts:

lake env lean --run VerifyMain.lean -- \
  --rules rules.json \
  --incompat incompatible.json \
  --infeasible infeasible.json \
  --exclusions fact-exclusions.json

Add --json for the versioned integration format. Run the complete build and regression suite with:

scripts/test.sh

The CLI exits with 0 for a verified contract, 1 for a safety failure, 2 for invalid arguments, and 3 for a load or structural-integrity failure.

Verification Contract

For a bundle bundle, MatCli proves:

MatCli.Verification.Soundness.verify_iff_contract :
  (MatCli.Verification.verify bundle).passed = true ↔
    MatCli.Verification.ContractHolds bundle

A passing report means:

• every referenced fact and action is declared;
• every admissible subset of declared facts is checked;
• no checked state derives conflicting verdicts for an action;
• no checked state obligates incompatible actions; and
• no checked state obligates an infeasible action.

This guarantee is universal over the finite domain declared by the bundle; the checker does not sample states. It does not establish the real-world truth of the input data, policy completeness, rule reachability, or requirements that have not been formalized.

Verification considers up to 2^n states for n declared facts before fact exclusions remove inadmissible states.

Reports and Evidence

Verification.Report contains the four check statuses, number of admissible states checked, total finding count, truncation status, and up to 100 typed findings. Findings identify the relevant state, action, rule IDs, source citations, artifact entry, and JSON Pointer-compatible path when applicable.

The evidence layer is itself proved sound: returned findings describe real violations, every failed report retains a finding, and passing agrees with an empty finding list.

Documentation

• Architecture explains the proof model, derivation semantics, checker, and soundness boundary.
• Domain integration describes artifact schemas, domain assumptions, and integration steps.

API

• MatCli.Verification.verify exhaustively verifies a bundle and returns a Verification.Report.
• MatCli.Artifacts.loadBundle loads and validates versioned JSON artifacts.
• MatCli.Artifacts.verifyLoaded verifies a loaded bundle while retaining its provenance and equality proof.
• MatCli.Artifacts.reportToJson projects a verification result to the stable JSON report format.

Contributing

Questions and bug reports are welcome in GitHub Issues. Pull requests are accepted; please keep changes focused and run scripts/test.sh before submitting one.

License

MIT © 2025 Jack Yang