BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//pretalx//cfp.devcon.org//devcon8//talk//XAD8FT
BEGIN:VTIMEZONE
TZID:IST
BEGIN:STANDARD
DTSTART:20000101T000000
RRULE:FREQ=YEARLY;BYMONTH=1
TZNAME:IST
TZOFFSETFROM:+0530
TZOFFSETTO:+0530
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:pretalx-devcon8-XAD8FT@cfp.devcon.org
DTSTART;TZID=IST:20261105T143000
DTEND;TZID=IST:20261105T145500
DESCRIPTION:Specs for confidential systems make security claims in prose: v
 alue is conserved\, no note can be spent twice. This talk is an experience
  report from machine-checking those claims for an open source shielded poo
 l spec in Lean 4: what verification actually involves\, what it costs a sm
 all team today\, and what's still open.
DTSTAMP:20261101T122934Z
LOCATION:Lotus Stage 2
SUMMARY:Formally Verifying a Shielded Pool in Lean 4 - Aaryamann Challani
URL:https://cfp.devcon.org/devcon8/talk/XAD8FT/
END:VEVENT
END:VCALENDAR