Hooray, my Erlang/Elixir-to-Lean project, Lynx, has already uncovered a bug in Erlang/OTP! I started exploring proofs about Erlang's calendar module. Some properties are straightforward. For example, converting seconds to days and time, then converting them back, should give us the original number of seconds: {days, time} = :calendar.seconds_to_daystime(seconds) days * 86400 + :calendar.time_to_seconds(time) == seconds We can also verify totality properties: that a function successfully returns a result for every input satisfying its preconditions. For example, every valid date should have an ISO week number: law iso_week_number_valid_date(date), requires: :calendar.valid_date(date), expects: is_tuple(:calendar.iso_week_number(date)) It turns out that this property couldn't be proven because iso_week_number/1 failed for January 1 and 2 of year 0000! Fortunately, this bug has already been fixed in Erlang/OTP. But the fact that we're already at the stage of uncovering real bugs with formal verification is incredibly exciting!