Knuckledragger

A proof assistant as a library that works directly over the smtlib logic via the z3 bindings.

https://www.kdrag.com

Egglog0 and Egglog

Extending egraphs with multipatterns leads to a mixed equality reasoning datalog engine

https://www.philipzucker.com/egglog0/ https://github.com/egraphs-good/egglog

CBAT

A weakest precondition binary verifier using the OCaml Binary Analysis Platform (BAP) as a framework. https://www.ndss-symposium.org/wp-content/uploads/bar2024-9-paper.pdf

https://github.com/draperlaboratory/cbat_tools

VIBES

https://github.com/draperlaboratory/VIBES

Awesome E-Graphs

A living reference of e-graph works

https://github.com/philzook58/awesome-egraphs

Pcode2C

Flexible binary verification and verified decompiler correspondence by lifting Ghidra PCode to a specialized C interpreter and then discharging obligations via CBMC.

https://github.com/philzook58/pcode2c

Flappy Bird MPC

https://github.com/philzook58/FlapPyBird-MPC

ZIPY - Inverted Pendulum YakShave

https://github.com/philzook58/cart_pole

https://cad.onshape.com/documents/0c9cb62ee8c98129226725b1/w/354a73b7d877f36fc06b8590/e/3254e7baca6a2053be4aa0fe

https://hackaday.io/project/158289-zipy-zipy-inverted-pendulum-yakshave

http://www.philipzucker.com/model-predictive-control-of-cartpole-in-openai-gym-using-osqp/

http://www.philipzucker.com/cartpole-camera-system-opencv-ps-eye-ir/

http://www.philipzucker.com/cartpole-maths/

http://www.philipzucker.com/cartpole-workin-boyeee/

Reality as a Service (RaaS)