Structural Comparison of Development Methodologies

Both emphasize "specification-driven development." Both share the fundamental structure of finalizing specifications in upstream phases and proceeding with design and implementation based on those specifications.

Waterfall specifications are written in natural language, making interpretation differences unavoidable. Formal methods use mathematical notation, greatly reducing room for interpretation. Additionally, waterfall specification contradictions are often discovered only in implementation/testing phases, whereas formal methods can detect them mechanically at the specification level.

Both recognize that creating a perfect specification from the start is difficult. Agile improves iteratively through post-release feedback, while formal methods increase precision through gradual specification refinement.

Agile values "working software over perfect specifications"; formal methods prioritize "correct specifications". Agile absorbs requirement uncertainty through post-release feedback, while formal methods make ambiguity and contradictions explicit and bring them into mechanically checkable form at the specification phase.

TDD verifies correctness through a finite set of test cases (inductive approach). Passing 100 tests does not eliminate the possibility of failure on the 101st case. When formal methods proceed all the way to theorem proving, they can deductively show that the properties formalized as proof obligations hold for all cases in scope.

TDD has another essential problem: the "specification" referenced when writing tests is never materialized. TDD's principle is to "write tests first," but where is the specification that guarantees the correctness of those test cases? In most cases, it exists only implicitly in the developer's mind. The test cases that get written are merely fragments of behavior that the developer believes "should probably work this way" — with no guarantee of completeness or accuracy.

The situation becomes even more problematic when tests are retrofitted to existing code. The test author reads the current implementation to infer "what this code should do," but what they are referencing is the implementation as-is — not the specification as-intended. If the code contains bugs, the tests will codify that buggy behavior as "correct." In other words, tests can become a mechanism that institutionalizes defects rather than guarding against them.

Formal methods structurally avoid this problem. Because specifications are explicitly written in a formal language such as VDM-SL, the "specification that grounds the tests" exists as a concrete artifact. Test cases are derived from the specification — not from the developer's tacit knowledge or the current state of the code.

However, this is not to say that formal methods negate TDD. It is also effective to use formal methods to make the specification precise, verify the properties selected for proof, and then employ TDD at the implementation level for quality control. The two have a complementary relationship.