Trusted systems and SW

Real SW applications need quotation, inspection
Algorithms for solving problems will be very varied
Proof language can be very simple
Proof checker + digital signature verifier = secure agent
Small trusted code base