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

• TM proofs/writing by Dan Briggs