We started a completely new PVS design of GDFM (Google Drive Formal Model) on 6 February 2015, with the aim of obtaining crystal clear proof obligations (TCCs), and elegant proofs. There is currently one library only, but we anticipate two:
Most recent dump and corresponding proof status |
Google DocsTor > Google Drive Formal Model >