---
title: 証明が通った。で、その仕様は正しいの？ golang.tokyo #44 Warashi
tags: 
author: [warashi](https://www.docswell.com/user/warashi)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/4EZLD24373.jpg?width=480
description: 証明が通った。で、その仕様は正しいの？ golang.tokyo #44 Warashi by warashi
published: August 05, 26
canonical: https://www.docswell.com/s/warashi/5N7GER-golang-tokyo-44
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/4EZLD24373.jpg)

証明が通った。
で、その仕様は正しいの？
Goの形式検証ツール Gobra に
decimal を検証させてみた
golang.tokyo #44 / Warashi
1


# Page. 2

![Page Image](https://bcdn.docswell.com/page/Y76W1V3Z7V.jpg)

白状します
AI に実装を書かせた
AI に証明も書かせた
通ってしまった
2


# Page. 3

![Page Image](https://bcdn.docswell.com/page/G75M4DL974.jpg)

自己紹介
太宰 晋之介 / GitHub: @Warashi
Finatext で証券ビジネスプラットフォーム BaaS の開発
テストケースの重複や網羅性を気にしなくてよくなりたい
3


# Page. 4

![Page Image](https://bcdn.docswell.com/page/9J29V8L5ER.jpg)

通ったからには、正しいのだろうか
そう思いたい。
ただ、そう言い切るには、Gobra が何を保証してくれる道具なのかを
知っていなければならない
4


# Page. 5

![Page Image](https://bcdn.docswell.com/page/DEY436Q6JM.jpg)

Gobra とは
ETH Zurich 製、Go のための自動コード検証ツール
Go のコードに事前条件と事後条件を書くと、あらゆる入力について成り立つか
を証明してくれる
// @ requires b != 0
// @ ensures res == a / b
func Div(a, b int) (res int) {
return a / b
}
Gobra found 0 errors.
golang.tokyo #43 「Goのコードを数学的に証明する」（@sollniss）で詳しく紹介されています
5


# Page. 6

![Page Image](https://bcdn.docswell.com/page/VJNYVZ2178.jpg)

題材：金額のための固定小数点 decimal
float では 0.1 すら表せない
// Decimal は coef * 10^-exp を表す固定小数点数
type Decimal struct {
coef int
exp int
}
10進の桁をそのまま持つので、誤差なく足し引きできる
6


# Page. 7

![Page Image](https://bcdn.docswell.com/page/YE9P6Z1YJ3.jpg)

実装の int と、表したい値
実装が扱うのは、有界な int の寄せ集め
意味として表したいのは、桁あふれしない数
この乖離をどう仕様に書く？
7


# Page. 8

![Page Image](https://bcdn.docswell.com/page/GE8DZ14KED.jpg)

integer 型（Gobra に最近入った）
ゴースト専用の数学的整数。上限も下限もない
// ghost.gobra : Go のビルドからは見えないファイル
ghost
decreases n
requires n >= 0
pure func pow10(n integer) (res integer) {
return n == 0 ? 1 : 10 * pow10(n-1)
}
.go には置けない。仕様の世界にだけ存在する
8


# Page. 9

![Page Image](https://bcdn.docswell.com/page/LELMDQ6P7R.jpg)

実装を仕様に結びつける
int で書いた実装が、 integer の理想と一致することを証明する
// @ requires n >= 0
// @ ensures res == pow10(n)
← integer の世界と接続
func Pow10(n int) (res int) {
res = 1
// @ invariant 0 <= i && i <= n
// @ invariant res == pow10(i)
for i := 0; i < n; i++ {
res = res * 10
}
return res
}
9


# Page. 10

![Page Image](https://bcdn.docswell.com/page/4JMYP152JW.jpg)

桁を揃えたときの値
// ghost.gobra
ghost
requires d.exp >= 0 && s >= d.exp
pure func scaled(d Decimal, s integer) integer {
return d.coef * pow10(s-integer(d.exp))
}
指数 s に揃えたときの係数。これも integer なので、
何桁ずらしても溢れない
10


# Page. 11

![Page Image](https://bcdn.docswell.com/page/PJR91L3579.jpg)

本題：桁を揃えた加算
// @ requires a.exp >= 0 && b.exp >= 0
// @ ensures res.exp >= a.exp && res.exp >= b.exp
// @ ensures scaled(res, res.exp) == scaled(a, res.exp) + scaled(b, res.exp)
func Add(a, b Decimal) (res Decimal) {
e := a.exp
if b.exp > e {
e = b.exp
}
ac := a.coef * Pow10(e-a.exp)
bc := b.coef * Pow10(e-b.exp)
return Decimal{coef: ac + bc, exp: e}
}
Gobra found 0 errors.
11


# Page. 12

![Page Image](https://bcdn.docswell.com/page/PEXQYW4XJX.jpg)

もう一つの Add
// @ ensures res.coef == a.coef+b.coef
// @ ensures res.exp == a.exp
func AddBuggy(a, b Decimal) (res Decimal) {
return Decimal{coef: a.coef + b.coef, exp: a.exp}
}
もっともらしく見えませんか？
12


# Page. 13

![Page Image](https://bcdn.docswell.com/page/3EK93VZ9ED.jpg)

こちらも 0 errors
Gobra found 0 errors.
0.1 + 0.02 = 0.3
桁を揃えていない。でも証明は通る
13


# Page. 14

![Page Image](https://bcdn.docswell.com/page/L73WGMD975.jpg)

ところで、さっきの Add は
$ gobra -p .
Gobra found 0 errors.
$ gobra -p . --overflow
intro.go:6
a / b might cause integer overflow.
decimal.go:10
res * 10 might cause integer overflow.
decimal.go:29
a.coef * Pow10(e-a.exp) might cause integer overflow.
buggy.go:7
{coef: a.coef + b.coef, ...} might cause integer overflow.
Gobra found 4 errors.
オーバーフロー検査は既定で無効。 Pow10(19) で溢れる
14


# Page. 15

![Page Image](https://bcdn.docswell.com/page/87DK16P8JG.jpg)

Gobra が保証していたもの
保証されたのは「実装が書いた仕様を満たす」ことだけだった
その仕様が欲しい性質を表しているかは、誰も確かめていない
どの設定で検証したかも、証明の中身の一部だった
AI は実装も仕様も書ける。だが「何を保証したいか」は決められない
仕様を書くことが、検証の本体
15


# Page. 16

![Page Image](https://bcdn.docswell.com/page/VJPKQYNWE8.jpg)

AI に書かせた、あの証明
いま手元にある decimal の証明は、通っている
書かれた仕様を、私はまだ読み切っていない
これから読む。そこからが検証だと思っている
16


# Page. 17

![Page Image](https://bcdn.docswell.com/page/2EVV5GK9EQ.jpg)

まとめ
Gobra：Go に事前条件と事後条件を書いて証明できる
integer：桁あふれしない数を仕様に書けるゴースト型
証明が通る ≠ 正しい：仕様のレビューは人間の仕事
Gobra 本体（公式 Docker イメージ ghcr.io/viperproject/gobra）
https://github.com/viperproject/gobra
golang.tokyo #43「Goのコードを数学的に証明する」
https://sollniss.github.io/presentations/20260218_golang.tokyo.43/
「自動推論シリーズスタート：Gobraでできること」
https://zenn.dev/finatext/articles/c4501622b2820b
「Gobra による複数粒度ロック証明への挑戦」
https://zenn.dev/finatext/articles/493a7e50-fb1e-4daf-a6de-5fbedb002842
17