|
|
|
|
|
|
by trenchgun
447 days 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. |
|
|