Code repositories

Creator	Link	Main language	Notes
bbchallenge	Link	?	Official bbchallenge deciders
@mxdys	Link	Rocq	Coq proof of BB(5) = 47,176,870. See Coq-BB5.
@mei	Link	Rocq, Rust, OCaml?	A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
Georgi Georgiev (Skelet)	Link	Pascal	See bbfind. Wrapped via bbfind-stdin by @wizord
@mxdys	Link	Rocq	Coq proof of some deciders and some solved machines in BB(6)
Mateusz Naściszewski @Mateon1	Link	Python 3	Accelerated TM simulators in Python utilizing memoization (like HashLife)
Mateusz Naściszewski @Mateon1	Link	Python 3	Forward segment TM decider by @Mateon1 (variant of Halting Segment)
Mateusz Naściszewski @Mateon1	Link	Python 3	Closed Position Set (CPS) TM decider implementation
Mateusz Naściszewski @Mateon1	Link	Python 3	Closed Tape Language (CTL) SAT Solver; TODO dependencies still Discord posts
@savask	Link	Haskell	Collection of deciders
@savask	Link	Haskell	Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program
@savask	Link	Haskell	Decider for Bouncers
@savask	Link	Haskell	Reproduction of @mxdys' RepWL_ES decider (repeated block decider)
@djmati1111	Link	Python 3	The first SAT-based Finite Automata Reduction (FAR) decider
Frans Faase	Link	C++	An early Closed Tape Language (CTL) verifier
@Iijil	Link	Go	Decider for Bouncers
@Iijil	Link	Go	Bruteforce Closed Tape Language (CTL) decider
@Iijil	Link	Go	Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider
@Iijil	Link	PHP	4-symbol to 2-symbol TM compiler
Jason Yuen @-d	Link	Lean 4	Some progress toward a FAR verifier checked by Lean
Matthew House @LegionMammal976	Link	Rust	An accelerated Bigfoot simulator
Nathan Fenner @nathanf	Link	Dafny, Rust?	Formally verified deciders using Dafny
Nathan Fenner @nathanf	Link	Dafny	Formally verified Closed Tape Language (CTL) verifier
Nathan Fenner @nathanf	Link	Rust	Closed Tape Language (CTL) decider
Nathan Fenner @nathanf	Link	Rust	Closed Position Set (CPS) simplification: uses less resources and is less strong
@nickdrozd	Link	?
@star	Link	?
Shawn Ligocki @sligocki	Link	Python 3, Rust, C++
Tony Guilfoyle	Link	C++
Justin Blanchard @UncombedCoconut	Link	Python 3
Justin Blanchard @UncombedCoconut	Link	Rust	Finite Automata Reduction (FAR) decider
Justin Blanchard @UncombedCoconut	Link	Python 3	Finite Automata Reduction (FAR) verifier
Pavel Kropitz @uni	Link	Rust
Dan Briggs	Link	Java	TM proofs/writing
Thomas Vigouroux @Vigoux	Link	Lean 4	An attempt at formalising results regarding Busy Beavers. Contains deciders and their proof of correctness.
@mxdys	Link	C++	Enumerating 7x2 TMs