Lean4 is a proof assistant with an extensive mathematical library. It's also a nice programming language that can be used for formal verification of software. In this impromptu session, I can help get an opinionated Lean4 setup running on your Linux computer using Nix and Neovim. If time permits, I can show how to prove simple theorems, and answer some of the questions that might come up.
See https://github.com/kowale/39c3-careful-whispers
location
NixOS assembly