Code repositories

Creator	Link	Notes
bbchallenge	https://github.com/bbchallenge/bbchallenge-deciders	Official bbchallenge deciders
@mxdys	https://github.com/ccz181078/Coq-BB5	Coq proof of BB(5) = 47,176,870. See Coq-BB5.
@mei	https://github.com/meithecatte/busycoq	A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
Georgi Georgiev (Skelet)	https://skelet.ludost.net/bb/	See bbfind and Skelet's 43 holdouts Wrapped via bbfind-stdin by @wizord
Mateusz Naściszewski @Mateon1	https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c	Accelerated TM simulators in Python utilizing memoization (like HashLife)
Mateusz Naściszewski @Mateon1	https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b	Forward segment TM decider by @Mateon1 (variant of Halting Segment)
Mateusz Naściszewski @Mateon1	https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc	Closed Position Set (CPS) TM decider implementation
Mateusz Naściszewski @Mateon1	https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3	Closed Tape Language (CTL) SAT Solver; TODO dependencies still Discord posts
@savask	https://github.com/savask/turing	Collection of deciders
@savask	https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f	Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program
@savask	https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72	Decider for Bouncers
@savask	https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697	Reproduction of @mxdys' RepWL_ES decider (repeated block decider)
@djmati1111	https://github.com/colette-b/bbchallenge	The first SAT-based Finite Automata Reduction (FAR) decider
Frans Faase	https://github.com/FransFaase/SymbolicTM	An early Closed Tape Language (CTL) verifier
@Iijil	https://github.com/Iijil1/Bouncers	Decider for Bouncers
@Iijil	https://github.com/Iijil1/Bruteforce-CTL	Bruteforce Closed Tape Language (CTL) decider
@Iijil	https://github.com/Iijil1/MITMWFAR	Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider
@Iijil	https://gist.github.com/Iijil1/d325da33be74a86ac2399c161a57166a	4-symbol to 2-symbol TM compiler
Jason Yuen @-d	https://github.com/int-y1/proofs/tree/master/BusyLean	Some progress toward a FAR verifier checked by Lean
Matthew House @LegionMammal976	https://github.com/LegionMammal978/bigfoot-sim	An accelerated Bigfoot simulator
Nathan Fenner @nathanf	https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders	Formally verified deciders using Dafny
Nathan Fenner @nathanf	https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier	Formally verified Closed Tape Language (CTL) verifier
Nathan Fenner @nathanf	https://github.com/Nathan-Fenner/bbchallenge-regexy-decider	Closed Tape Language (CTL) decider
Nathan Fenner @nathanf	https://github.com/Nathan-Fenner/bb-simple-n-gram-cps	Dramatic Closed Position Set (CPS) simplification (much less resource-intensive and not as strong)
@nickdrozd	https://github.com/nickdrozd/busy-beaver-stuff
@start	https://github.com/phinanix/busy-beavers
Shawn Ligocki @sligocki	https://github.com/sligocki/busy-beaver
Tony Guilfoyle	https://github.com/TonyGuil/bbchallenge
Justin Blanchard @UncombedCoconut	https://github.com/uncombedcoconut/bbchallenge
Justin Blanchard @UncombedCoconut	https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction	Finite Automata Reducion (FAR) decider
Justin Blanchard @UncombedCoconut	https://github.com/UncombedCoconut/bbchallenge-nfa-verification	Finite Automata Reducion (FAR) verifier
Pavel Kropitz @uni	https://github.com/univerz/bbc
Dan Briggs	https://github.com/danbriggs/Turing	TM proofs/writing