這個是信任，你底下講的是資安，也就是你的spec，可以是可信任的，但是你的implementation，如果沒有自帶證明或者是沒有用什麼proof assistant跑過，可能實作的時候會跑掉。
這個是信任，你底下講的是資安，也就是你的spec，可以是可信任的，但是你的implementation，如果沒有自帶證明或者是沒有用什麼proof assistant跑過，可能實作的時候會跑掉。