3 ms·
Verifiers can be based on a small proven kernel. That is not really the issue. The issue is writing the formal specification. Formal verification is in nutshel
by trenchgun 2y ago
Verifiers can be based on a small proven kernel. That is not really the issue.
The issue is writing the formal specification. Formal verification is in nutshell just proving the equivalence of two different formal constructs: one that is called the spec and one that is called the system (or program). Writing specs is hard.