Using the design ideas implemented in Metamath, Raph Levien has implemented what might be the smallest proof checker in the world, mmverify.py, at only 500 lines of Python code.
The free software developer resource Advogato is based on a novel approach to attack-resistant trust metrics of Raph Levien.