[nextos]

What formal methods did you use?

[exdsq]

Combination of Agda, Isabelle, Coq, and TLA+ depending on the team - I mostly interacted with TLA+ and the compiled Haskell from Agda specs :)

[dwohnitmok]

Wow definitely want to pick your brain. How large/# of LOC were the Agda, Isabelle, and Coq specs? What industry was this?

[exdsq]

Blockchain - two repos with specs are:

* https://github.com/input-output-hk/cardano-ledger

* https://github.com/input-output-hk/plutus

There's quite a few recent Isabelle repos such as https://github.com/input-output-hk/high-assurance-legacy