20 lines
728 B
Markdown
20 lines
728 B
Markdown
# 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)
|