This lecture introduces the SecChisel framework, which verifies security properties of secure processor architectures at design-time. It covers Chisel as a hardware construction language, information flow tracking, security lattices, security tags, FIRRTL, SMT-LIB, and evaluation using AES within a RISC-V Rocket Chip. The framework aims to detect information leaks and hardware bugs efficiently, without adding runtime components.