As much as possible mechanical (non-LLM) verification of equivalence that generates good diagnostic messages, mechanical translation steps that generate good diagnostic messages, a good memory system to reduce rework... (edit: and mechanical coverage measurement)