Meeting Notes 0

• Project is mine
• Find what is cool in the project area
• Rigour for validity in important areas
• Cryptography - logical errors can be exploited, happened a while ago: Needham & Schroeder
• Defining security
• Making sure everything is true
• Computer formalisation - framework of yes/no to validate truth
• Proof assistants! <- e.g. Lean, Coq, prototype verification system (PVS) used in NASA!
• Backwards search logic
• Computer-verified proof
• FORMAL METHODS - popular articles, formal bits, news
• Find one exciting thing then back-engineer
• 6-15 references