Code repositories
This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them.
- The official bbchallenge deciders repo
- Coq-BB5 by @mxdys
- A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei
- bbfind by Skelet wrapped via bbfind-stdin by @wizord
- Accelerated TM simulators in Python utilizing memoization (like HashLife), by @Mateon1
- Forward segment TM decider by @Mateon1 (variant of Halting Segment)
- Closed Position Set (CPS) TM decider by @Mateon1
- SAT Solver CTL code by @Mateon1; TODO dependencies still in Discord posts
- The closed position set decider, reverse-engineered from Skelet's program, by @savask
- Bouncers decider, by @savask
- Reproduction of mxdys' repeated blocks decider, by @savask
- The first SAT-based CTL/FAR decider, by @djmati1111
- An early CTL verifier (regex-based) by Frans Faase
- Bouncers decider, by @Iijil
- Bruteforce-CTL decider, by @Iijil
- Meet-in-the-Middle Weighted Finite Automata... Reduction... by @Iijil
- Some progress toward a FAR verifier checked by Lean, by @-d
- An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978
- Deciders formally verified using Dafny, by @nathanf
- CTL decider by @nathanf
- A dramatic simplification of CPS (much less resource-intensive and not as strong) by @nathanf
- A formally verified CTL checker by @nathanf
- https://github.com/nickdrozd/busy-beaver-stuff
- https://github.com/phinanix/busy-beavers
- https://github.com/sligocki/busy-beaver
- https://github.com/TonyGuil/bbchallenge
- https://github.com/uncombedcoconut/bbchallenge
- https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction
- https://github.com/UncombedCoconut/bbchallenge-nfa-verification
- https://github.com/univerz/bbc