Queue M30: survey how much algorithm correctness can be machine-checked - #92

Merged

MikeGrier merged 9 commits into

mainfrom

mikegrier/formal-methods-survey

Sep 17, 2026

Commits on Sep 17, 2026

docs: queue M23, a survey of how much algorithm correctness can be machine-checked

Mike Grier
and
Copilot
committed
49009f4
docs: renumber the formal-methods milestone M23 -> M30, which was taken

Mike Grier
and
Copilot
committed
21bcc7f
docs: correct the pilot's premise, which named the wrong reason and the wrong shape

Mike Grier
and
Copilot
committed
d4c30e4
docs: give the pilot a refinement criterion, and move the rationale out of the queue

Mike Grier
and
Copilot
committed
e1c8d64
docs: do the tracker update rather than queue it, and finish emptying the checklist

Mike Grier
and
Copilot
committed
a6a9a8f
docs: move M30's rationale to Tier 2, where pre-decision context belongs

Mike Grier
and
Copilot
committed
45a1849
docs: attribute the shape scope to D-29, and stop overstating what two tools see

Mike Grier
and
Copilot
committed
562bc6d
docs: a green run on the unmodified model would mean the model is unfaithful

Mike Grier
and
Copilot
committed
239cc86
docs: require M30.5 to state the cost its own heading promises

Mike Grier
and
Copilot
committed
e5bc9c7