What is formal verification?
- Author
- CRYPTO PORT Editorial
- Published
- Updated
- Reading time
- 6 min
In short
Formal verification states the properties code must satisfy in mathematical terms and proves they hold for every possible input. Tests can only show that nothing broke in the cases you tried; a proof covers all of them. The limit is that it proves only the properties you wrote down — an omission in the specification stays invisible.
Key points
- Proves stated properties across all possible inputs
- Unlike testing, it is not limited to the cases tried
- Only the properties you specify are covered
- Usually applied to the most critical components
Definition
A verification method that expresses the properties a program must satisfy as a formal specification, then proves mathematically that they hold across every execution path and input.
Ordinary testing runs a set of inputs and checks the results, which says nothing about the inputs you did not try. Formal verification works the other way round: you write a property — say, that a function can never change total supply — and prove that no input exists which violates it.
Smart contracts are hard to patch after deployment, handle large sums and are comparatively short, a combination that suits this approach well. It is increasingly applied to core pieces: token accounting, the relationship between collateral and debt, and how privileges may change. It is also used on consensus and staking designs.
The limits are equally clear. Only the stated properties are proved, so an assumption nobody wrote down can still fail. Behaviour that emerges from composing with external protocols, and the actions a privileged operator is permitted to take, are usually outside the verified boundary.
For a user, the takeaway is not to read 'formally verified' as unconditional safety. Look for a published statement of which components were covered and which properties were proved. Verification with a defined scope, alongside audits and an active bounty, is as thorough as current practice gets.
Watch out for
- · Do not read 'formally verified' as safe — check which components and properties were covered
- · Assume composition with other protocols and operator privileges sit outside the verified boundary
- · Never size a position on any one of verification, audit or bounty alone