|
|
|
|
|
|
by johnbender
1694 days ago
|
|
|
In Coq the user generally writes meta programs to generate proofs as programs at varying levels of automation (Ltac scripts). Here they used IC3 to automatically produce proof that their state based model of paxos satisfies the invariant. In principle one could build an automated proof system for a state machine-esque formalism written in Coq using Ltac but that would be a nightmare in practice. |
|
|