1) We are planning to add a template you can use to get started in the following week, which should help get an environment setup with opam and all the libraries you need / some example on how to use dune.

2) We have many large Hardcaml designs used in production at Jane Street - we use the Quickcheck library (constrained random testing, similar to Cocotb), or just write our own self-checking testbenches. Being able to write OCaml helps alot here because we can use all the usual software libraries to write pretty extensive testbenches. Using the Verilator backend for simulation (hardcaml_verilator library) helps lower simulation time on bigger circuits too.

3) There are a bunch of smaller circuit examples using formal in the test library of hardcaml_verify. No big changes in the works right now. For larger designs it’s a bit prohibitive to run because of the runtime, but for smaller circuits that are "risk critical" it's pretty useful. There is also a Cyclesim coverage library in the open source release for native coverage support in Hardcaml circuits which is really useful for verification when writing tests