Chapters 2 to 15 and appendix B of the book Symmetry in the Narya proof assistant: 888 of 917 blocks have a formal statement and a proof, 19 blocks that are false as printed have counterexamples and corrected statements.
Proof sessions in Narya for agents: holes with contexts and types, split, try and solve, search over the project, and rechecks of only the changed commands.
A gate that accepts a redstone layout only with a machine-checkable proof that it computes its Verilog specification, with 92 interactive 3D layout viewers.