> The other extreme would be a GUI program. Can a button be formally verified (or failed), if due to poor graphic design it may or may not look like a button?

> The other extreme would be a GUI program. Can a button be formally verified (or failed), if due to poor graphic design it may or may not look like a button? Another "other extreme": create the source for a new database manager that formally matches the behavior of another database manager, that you only have object code for. :)