The KeYmaera X developers are incredibly thankful for the helpful feedback on its earlier versions from all the users everywhere, but especially the power users:
If you have a question about KeYmaera X, either ask on the KeYmaera X mailing list or directly ask the right person based on the primary responsibilities listed below.
Stefan Mitsch: user interface, tactic library, tactic tracing, lemma mechanism, command line interface, ModelPlex tactics, HyDRA web service API, tactic task scheduler, Mathematica interface, SMT interface, data storage design, performance improvements
Nathan Fulton: Bellerophon tactic framework, tactic parser, tactic extraction, lexer and declarations parser, Mathematica interface, HyDRA web service API
André Platzer: prover core, differential dynamic logic parser+printer, unification-based calculus auto-tactics, forward tactics and engine
Brandon Bohrer: data model and proof storage database, security
Yong Kiam Tan: automatic simplification tactics, polynomial arithmetic normalization, arithmetic ordering heuristics
Ran Ji: Polya SMT interface, C code generation