Coq proofassistant Projects

It's always a pleasant surprise to see people using Coq and other formal verification technology. We need more rigor in programming! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [1] (a variant of another useful tactic called `magic` which solve goals with existentials) which can automatically prove the theorem from the article.
[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

kami
A Platform for HighLevel Parametric Hardware Specification and its Modular Verification (by mitplv)
Project mention: There's an ongoing effort to rewrite Principia Mathematica using Coq  reddit.com/r/math  20211203There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mitplv/koika), Kami (https://github.com/mitplv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/projectoak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.

Zigi
The context switching struggle is real. Zigi makes context switching a thing of the past. It monitors Jira and GitHub updates, pings you when PRs need approval and lets you take fast actions  all directly from Slack!