| 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 Reducion (FAR) decider
|
| Justin Blanchard @UncombedCoconut
|
Link
|
Python 3
|
Finite Automata Reducion (FAR) verifier
|
| Pavel Kropitz @uni
|
Link
|
Rust
|
|
| Dan Briggs
|
Link
|
Java
|
TM proofs/writing
|
| @mxdys
|
Link
|
C++
|
Enumerating 7x2 TMs
|