The Mathematicians, June 11: forms.gle/w16jkmsMqB2g...
The Builders, June 12: forms.gle/PsxPkq3x2pES...
2/3 Veil's approach: write a model once, then apply model checking, SMT-based proofs, and interactive theorem proving from a single specification. Its embedding in Lean means a very small trusted computing base.