Proving autonomous driving safety: T2 and Imiron launch joint project to validate safety using formal methods.

〜Towards the Social Implementation of Next-Generation Mobility: Strengthening Safety Evaluation and Logical Explainability Through a Mathematical Approach~

T2 Inc. (Chiyoda-ku, Tokyo; CEO: Masatomo Kumabe; hereinafter “T2”) and Imiron Co., Ltd. (Chiyoda-ku, Tokyo; CEO: Masakazu Adachi; hereinafter “Imiron”) will commence a joint verification project for formal safety argumentation aimed at obtaining Level 4 autonomous driving approval, starting in August 2025. This initiative is a globally advanced challenge to rigorously prove the safety of autonomous vehicles through formal methods and mathematical proof, and its application to practical operation will be the first attempt in Japan.

1. Background

T2 is currently seeking approval from Japan’s Ministry of Land, Infrastructure, Transport and Tourism (MLIT) and other authorities for autonomous truck mainline transportation. However, traditional methods have limitations in concisely and logically explaining safety to obtain approval, which requires vast amounts of driving data to be presented on limited pages.

Therefore, this collaboration was formed after confirming the effectiveness of a mathematical safety argumentation framework. This framework was built by Imiron, leveraging their advanced theories and achievements in safety argumentation, and utilizing research findings on “GA-RSS (Goal-Aware Responsibility-Sensitive Safety)*1” from the National Institute of Informatics.

*1 I. Hasuo et al., “Goal-Aware RSS for Complex Scenarios via Program Logic,” in IEEE Transactions on Intelligent Vehicles, vol. 8, no. 4, pp. 3040-3072, April 2023, doi: 10.1109/TIV.2022.3169762.

2. Advantages of Formal Methods and Mathematical Proof

Traditional safety evaluations primarily rely on a statistical verification approach, such as “no accidents over 10 million kilometers of driving.” In contrast, the formal methods adopted in this project allow for mathematically modeling driving scenarios—like collision avoidance and safe stopping—to logically derive that safety is guaranteed.

The GA-RSS research, utilized by Imiron, is an extension of the globally recognized “RSS (Responsibility-Sensitive Safety)” and can be applied to complex, realistic driving scenarios that include intricate driving goals (e.g., merging/splitting before and after toll gates).

This enables T2 to provide the high level of safety explanation required by MLIT, using a transparent logical and formal approach.

3. Project Overview

Date: August 2025

Objective: To strengthen safety argumentation through a mathematical approach for autonomous truck operation and to build a safety explanation framework for social implementation.

T2 will provide autonomous driving routes and scenarios. Imiron will establish a mechanism that demonstrates “why autonomous driving is safe” using mathematics and logic.

• Scenario formalization: Defining how the vehicle should behave under various traffic rules and road conditions using unambiguous mathematical formulas and logic.
• Argumentation structuring: Clearly organizing reasons and evidence to explain safety in an easily understandable way to others.

Expected Outcomes:

• Support for obtaining approval through Japan’s first practical application of logical proof.
• A model case for the industrial implementation of formal methods in autonomous driving.
• Establishment of T2’s advanced safety argumentation methods.
• Ripple effects on future academic collaborations (e.g., paper publications).

For autonomous driving to become deeply integrated into society, its safety must be demonstrated in a way that everyone can understand and accept. Through safety argumentation based on formal methods, we aim to achieve “explainable safety” and bridge the gap between technology and trust. This collaboration will lay the groundwork for a society where autonomous driving can be embraced with confidence.