Proof

Prove correctness, then optimality

Treat correctness as a relation between a program and a stated contract. First say exactly what must be true. Then give a logical argument that the code makes it true for every allowed case.

Treat correctness as the entry condition for comparison. An incorrect solution is not a candidate for "better." Only after the chosen implementation is proved correct may its optimality be considered.

Treat optimality as a universal claim. Define the allowed solution space and what "strictly better" means, then prove that no other correct solution in that space is strictly better. Comparing only a few remembered alternatives is not an optimality proof.

Write proofs that a person can inspect. Use definitions, stated assumptions, language and library semantics, and proofs already established for dependencies. Do not replace reasoning with a tool result. A passing test, compiler, type checker, static analyzer, model checker, or theorem prover belongs to another validation layer. It does not stand in for the written proof required here.

Keep the proof beside the code it explains. Do not claim that a function, module, change, or project is correct or optimal while the matching obligation is open or disproved.

Set the production boundary

Find the code that the project owns and that runs to provide the production result. Read manifests, entry points, package boundaries, build settings, and deployment paths to find it.

Include every first-party production module and every callable body inside it: