02 — Framework · Failure mode
Reading 'formally verified' as unconditional
A project advertises formal verification and the claim is real but scoped — bounded by stated hypotheses, covering some components and not others. Bugs have been found by conformance testing in exactly the areas a verification effort did not cover.
Mitigation
Ask what was verified, against which specification, under what hypotheses, and what was explicitly out of scope. A precise, bounded claim is a good sign; an unqualified one is not.
Related pages
Cite this page
MarketComp (2026). Reading 'formally verified' as unconditional. The ZK Field Manual (Version 1.3). MarketComp. https://zkpick.com/frameworks/failure-modes/reading-formally-verified-as-unconditional/
@misc{zkfieldmanual-reading-formally-verified-as-uncondition,
title = {Reading 'formally verified' as unconditional — The ZK Field Manual},
author = {MarketComp},
year = {2026},
version = {1.3},
howpublished = {\url{https://zkpick.com/frameworks/failure-modes/reading-formally-verified-as-unconditional/}},
note = {Accessed: YYYY-MM-DD}
}