|
|
|
|
|
|
by touisteur
1209 days ago
|
|
|
Although it would be a great exercise in hybrid SPARK+Coq proof. If (that's a big if) you can specify your algorithm in SPARK then (I think) you can use either the SPARK automated/guided prover, or when it can't discharge the proof, use some predefined lemmas, and barring that go down to the interactive Coq environment (or Isabelle, I've seen it done once) and discharge the verification conditions. Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/. |
|
|