|
|
|
|
|
|
by nickpsecurity
3549 days ago
|
|
|
Far as prover verification, these people mostly solved it: https://www.cs.utexas.edu/users/jared/milawa/Web/ They start with small logics you can do by hand in verified code. They gradually build on them, one layer at a time, increasingly sophisticated logics until they have a useful theorem prover in first-order logic. I also found a HOL-to-FOL converter. Since most of their stuff is HOL, that means we're almost done at that point for the verification chain. |
|
|