The problem
AI clinical decision tools are deployed across health systems with no mathematical proof that they cannot recommend harmful treatment sequences. The MHRA 2026 AI device framework requires safety cases. No accepted formal methodology exists.
Vitacore approach
A probabilistic timed automaton framework for formally specifying and verifying the behaviour of AI clinical decision systems. Model checking provides mathematical guarantees about alarm safety and treatment sequence validity.
Output
Target venue: npj Digital Medicine · BMJ Health & Care Informatics · IEEE TDSC.
Theory paper: 6–8 weeks. No dataset required.