# docs/formal/proofs/

One of the four standalone reports — *StarForth Formal Verification Report*.

- **[main.tex](main.tex)** — Report entry point. Mirrors the Isabelle/HOL
  theory corpus in `proof/` (24 theory files: base definitions,
  correctness, 7 physics feedback loops, word-category proofs, and the
  5-theory word-ACL proof set).

Built via `make -C docs/formal proofs`; output lands at
`docs/formal/build/proofs/main.pdf`.

## See also

- [`proof/README.md`](../../../proof/README.md) — the Isabelle/HOL theory
  files this report presents.
- [`docs/formal/README.md`](../README.md) — the three-group publication
  structure this report belongs to (standalone reports).
- [Project root](../../../README.md)