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, task scheduler, Mathematica interface, SMT interface
André Platzer: prover core, parser+printer, unification-based calculus tactics, forward tactics
Brandon Bohrer: proof tree UI data, proof database, security, tactic information for UI
Yong Kiam Tan: simplification tactics, polynomial arithmetic normalization, arithmetic ordering heuristics
Ran Ji: Polya SMT interface, C code generation