In this presentation, I'll talk about Cryptis, a tool we have been developing for verifying systems that feature cryptographic components, such as a key-value store server that connects to clients using some encryption protocol.  Cryptis is a separation logic embedded in the Coq proof assistant, which can be used to describe the implementation of protocols and systems that use these protocols.   Cryptis can check proofs of correctness involving arguments in the symbolic model of cryptography, thus guaranteeing that protocols can deliver strong security guarantees.   Bio:  Arthur Azevedo de Amorim joined the Department of Computer Science at RIT in 2023 as an assistant professor.  His research interests revolve around the use of programming-language and software-verification techniques to improve the security and reliability of software.