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.
Nathan Fulton: Bellerophon tactic framework, tactic parser, tactic extraction, lexer and declarations parser, Mathematica interface, HyDRA web service API
Stefan Mitsch: user interface, tactic library, tactic tracing, lemma mechanism, command line, ModelPlex tactics, HyDRA web service API, tactic task scheduler, Mathematica interface, SMT interface, data storage design
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