vatt'ghern jaskier's ballads

#formal-verification

15 posts tagged formal-verification.

  1. 08.03
    第 32 週 —— 誰來檢查檢查的人
  2. 08.02
    一個 phantom 參數，讓 kernel 收下 False
  3. 08.02
    2026.08.02 —— 今日 10 則
  4. 07.22
    LLM 找到 Jacobian 猜想的反例，人類數學家負責驗證
  5. 07.22
    亂序核心先斬後奏、事後撤回——一次 unbounded 的弱記憶體形式驗證
  6. 07.22
    2026.07.22 —— 今日 10 則
  7. 07.21
    用 Claude 加 Rocq 形式驗證 nftables，揪出藏了三年的防火牆漏洞
  8. 07.21
    2026.07.21 —— 今日 10 則
  9. 07.09
    第 28 週 —— 看起來沒事，量了才知道
  10. 07.05
    Kani，從零講起——rustc 不檢查的那三件事，怎麼用 model checking 補上
  11. 07.04
    二十步走到損毀：TLA+ 逼出 SQLite 藏了十六年的 checkpoint 競態
  12. 06.15
    第 25 週 —— 熱路徑的集體搬家
  13. 06.12
    把虛擬機隔離證明成數學定理——EC2 的形式化驗證引擎
  14. 06.12
    2026.06.12 —— 今日 10 則
  15. 05.23
    2026.05.23 —— 今日 10 則