https://github.com/wilbowma/cur formal specification and verification of hardware dependently typed programming language with compile time malloc/free https://github.com/GaloisInc/lean-llvm llvm support for lean theorem prover https://github.com/gallais/generic-syntax agda repo for a type safe universe of syntaxes https://github.com/crypto-agda/protocols shallow embedding of protocols with agda dependent types https://github.com/cedille/cedille https://github.com/vasilisp/inez constraint solver
HOL Interactive Theorem Prover The E Theorem Prover Software Foundations Vellvm - Verifying the LLVM - Galois, Inc. rntz/datafun: Research on integrating datalog & lambda calculus via monoton wrightverification/README.md at master · patio11/wrightverification Verification Mentoring Workshop: Session 1 - YouTube
lvm/build-supercollider: A dead simple script that builds and installs Supe A formally verified high-level synthesis tool based on CompCert and written [2010.00774] Proof Repair Across Type Equivalences tevador/RandomX: Proof of work algorithm based on random code execution https://hol-theorem-prover.org/ http://acl2s.ccs.neu.edu/acl2s/doc/ homotopy type theory in agdaMath a little taste of dependent types 4. Propositional Logic in Lean — Logic and Proof 0.1 documentation
https://itp19.cecs.pdx.edu/ conference on interactive theorem proving : )
https://plv.csail.mit.edu/blog/ blog from adam chlipapa's lab! http://www.cse.chalmers.se/research/group/logic/publications.html
https://www.stephanboyer.com/ a great article for approaching theorem proving is featured here. Look to learn from this as needed!