I'm working on circuit construction and found the tool nMigen https://m-labs.hk/gateware/nmigen/
nMigen is a Python toolbox for building complex digital hardware. nMigen offers Bounded Model Checking and formal verification tool checkers for circuits. You can, for example, guarantee that a certain signal state is always true (definitions) or that some combination of circuit signals never occur (logic checks). Thus you can formally verify the circuits. While it seems crazy to think about proofs and Lean checking "to the metal" level I think you'll be surprised at how fast the industry is changing. Truly complex hardware, such as full circuit boards faster than most laptops, has hit the under-100 dollar range. There are several people working on RISC-V processors in open source: https://hackaday.io/project/178826-pineapple-one https://www.youtube.com/watch?v=YgXJf8c5PLo&list=PLEeZWGE3PwbZTypHq00G-yEX8TEI95lw4 RISC-V is an open source instruction set that allows user-extensible instructions (e.g. a check-proof instruction that side-loads proof-check code for an algorithm into the FPGA). The RISC-V instruction set is MUCH simpler than the x86, making it easier to write and verify the semantics. I now have 2 boards that each have both a CPU and an FPGA on the same board. I can "reprogram the FPGA" directly from the CPU, thus I can "side load a proof" based on the algorithm the CPU is running. So the circuits are correct that implement the proof checker and the RISC-V instruction set. The proof checker from LEAN checks the proof for the current algorithm while the algorithm executes. The algorithm and proof are packaged together in an AES module so they can't be tampered with. The "proof state" can be maintained so it can be input as an axiom to the next algorithm, "chaining" the proofs thru the program. One of these years I hope to have a "down to the metal" real-time proof-checked GCD algorithm running in Axiom. Longer term, as each Axiom algorithm is proven, LEAN can use Axiom's mathematics "at a higher level". There is still a long way to go, of course. This is about as hard are research gets I think, even PhD research. But it has the long-term potential of eliminating bugs at all levels which I think will change the industry. Tim