# Historical documents (unsupported)

Files in this directory and under `experimental/legacy-formalverifml/` are retained for archaeology only.

They are **not** release evidence for LeanVerifier v0.1.0.

## Contents

| Path | Note |
|------|------|
| `ENTERPRISE_IMPLEMENTATION_SUMMARY.md` | Withdrawn enterprise / production claims |
| `DOCUMENTATION_IMPROVEMENT_SUMMARY.md` | Prior documentation campaign notes |
| `test_report.txt`, `test_config.json` | Failing / unsupported historical runs |
| `test_results_*.json`, `enterprise_test_config.json` | Unsupported feature test dumps — not attestation artifacts |

An empty `enterprise_test_report.txt` was deleted during recovery cleanup (no archival content).

## Experimental code

See `experimental/legacy-formalverifml/` for the former FormalVerifML Lean tree, translator, and webapp.
The webapp’s upload → `lake build` path is quarantined; see [SECURITY.md](../../SECURITY.md).

## Prohibited claim language

Active docs must not claim production-ready, enterprise-grade, encryption-backed product security, 100M+ parameter verification, or distributed verification as supported features. Mentions that explicitly withdraw or quarantine those phrases are allowed.