Pinned Repositories
chatterbox
A chat thingy
clock
Clock is a small library for mocking time in Go.
crypto-graphically
Experimental graph-based visual representation and proof method for cryptographic interactions
curve25519-verilog
Beginnings of a Verilog implementation of Curve25519.
dename
NameCoin-style names using consensus instead of proof of work
salsa20
An implementation of djb-s salsa20 in 45 lines of human-readable C code
torch
Probably not the TOR client you are looking for.
vindicat
Mesh networking based on maintaining a graph of link objects signed by peers. WIP.
andres-erbsen's Repositories
andres-erbsen/dename
NameCoin-style names using consensus instead of proof of work
andres-erbsen/clock
Clock is a small library for mocking time in Go.
andres-erbsen/crypto-graphically
Experimental graph-based visual representation and proof method for cryptographic interactions
andres-erbsen/chatterbox
A chat thingy
andres-erbsen/torch
Probably not the TOR client you are looking for.
andres-erbsen/safecurves-primes
Checking the SafeCurves primes in Coq
andres-erbsen/certifying-derivation-of-state-machines-from-coroutines
andres-erbsen/cogs
Dotfiles and small scripts mostly used in my laptop
andres-erbsen/coq-experiments
gists that build
andres-erbsen/dename-writeup
andres-erbsen/listproxy
HTTPS reverse proxy to enforce authrorization using MIT Moira lists
andres-erbsen/protobuf
Protocol Buffers for Go with Gadgets
andres-erbsen/rrtcp
Realtime audio-over-TCP that sucks less
andres-erbsen/adaptagrams
Libraries for constraint-based layout and connector routing for diagrams.
andres-erbsen/coq-debian-build-scripts
Various scripts for packaging versions of Coq into a ppa
andres-erbsen/curve25519-donna
Implementations of a fast Elliptic-curve Diffie-Hellman primitive
andres-erbsen/drake
A planning, control, and analysis toolbox for nonlinear dynamical systems. More info at
andres-erbsen/drake-dynamic-soaring
andres-erbsen/drake-shambhala
Exemplifies various ways to open a pathway to using Drake in your own project.
andres-erbsen/email
andres-erbsen/frap
Formal Reasoning About Programs
andres-erbsen/hacspec
andres-erbsen/micro-mitten
you might not need your garbage collector
andres-erbsen/PKGBUILDs
andres-erbsen/QuickChick
Randomized Property-Based Testing Plugin for Coq
andres-erbsen/riscv-coq
RISC-V Specification in Coq
andres-erbsen/simple-https-server
a HTTPS server as simple as `python -m SimpleHTTPServer' (uses LetsEncrypt)
andres-erbsen/smtcoq
Communication between Coq and SAT/SMT solvers
andres-erbsen/VST
Verified Software Toolchain
andres-erbsen/yosys
Yosys Open SYnthesis Suite