{"id":42329,"date":"2025-07-18T12:39:07","date_gmt":"2025-07-18T03:39:07","guid":{"rendered":"https:\/\/sipo.tokyo\/?p=42329"},"modified":"2025-07-18T12:40:41","modified_gmt":"2025-07-18T03:40:41","slug":"post-42329","status":"publish","type":"post","link":"https:\/\/sipo.tokyo\/?p=42329","title":{"rendered":"\u30ab\u30eb\u30c0\u30ce\u306b\u8a2a\u308c\u308b\u65b0\u6642\u4ee3\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u5b8c\u5168\u81ea\u52d5\u5316\u3078"},"content":{"rendered":"\n<div class=\"dp_toc_container pos-before_first_h allow-toggle\" role=\"navigation\" data-margin=\"30\"><p class=\"toc_title_block\"><span class=\"toc_title icon-list\">INDEX<\/span><span class=\"toc_toggle icon-up-open\" role=\"button\"><\/span><\/p><ul class=\"dp_toc_ul has_title\"><li><a href=\"#e382abe383abe38380e3838ee381abe8a8aae3828ce3828be696b0e69982e4bba3efbc9ae382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388-1\">\u30ab\u30eb\u30c0\u30ce\u306b\u8a2a\u308c\u308b\u65b0\u6642\u4ee3\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u5b8c\u5168\u81ea\u52d5\u5316\u3078<\/a><ul><li><a href=\"#lean4e381a8z3e3818ce58887e3828ae68b93e3818fe38081e9968be799bae88085e38395e383ace383b3e38389e383aae383bce381aae38395e382a9e383bce3839e-2\">Lean4\u3068Z3\u304c\u5207\u308a\u62d3\u304f\u3001\u958b\u767a\u8005\u30d5\u30ec\u30f3\u30c9\u30ea\u30fc\u306a\u30d5\u30a9\u30fc\u30de\u30eb\u30fb\u30d9\u30ea\u30d5\u30a3\u30b1\u30fc\u30b7\u30e7\u30f3<\/a><\/li><li><a href=\"#e381aae3819ce5bda2e5bc8fe79a84e6a49ce8a8bce3818ce5bf85e8a681e381aae381aee3818befbc9f-3\">\u306a\u305c\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5fc5\u8981\u306a\u306e\u304b\uff1f<\/a><\/li><li><a href=\"#e382b2e383bce383a0e38381e382a7e383b3e382b8e383a3e383bcefbc9alean4efbc8bz3e381abe38288e3828be5ae8ce585a8e887aae58b95e58c96-4\">\u30b2\u30fc\u30e0\u30c1\u30a7\u30f3\u30b8\u30e3\u30fc\uff1aLean4\uff0bZ3\u306b\u3088\u308b\u5b8c\u5168\u81ea\u52d5\u5316<\/a><\/li><li><a href=\"#e6a49ce8a8bce4be8befbc9ae38399e382b9e38386e382a3e383b3e382b0e382b3e383b3e38388e383a9e382afe38388e381aee890bde381a8e38197e7a9b4-5\">\u691c\u8a3c\u4f8b\uff1a\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u843d\u3068\u3057\u7a74<\/a><\/li><li><a href=\"#e9968be799bae78ab6e6b381e381a8e4bb8ae5be8ce381aee5b195e69c9b-6\">\u958b\u767a\u72b6\u6cc1\u3068\u4eca\u5f8c\u306e\u5c55\u671b<\/a><\/li><li><a href=\"#e381bee381a8e38281efbc9ae382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388e381aee69caae69da5e381afe3808ce8a8bce6988ee58faf-7\">\u307e\u3068\u3081\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u672a\u6765\u306f\u300c\u8a3c\u660e\u53ef\u80fd\u306a\u5b89\u5168\u6027\u300d\u3078<\/a><\/li><\/ul><\/li><li><a href=\"#ioge38396e383ade382b0e3808ce382abe383abe38380e3838ee381abe3818ae38191e3828be382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382af-8\">IOG\u30d6\u30ed\u30b0\u300c\u30ab\u30eb\u30c0\u30ce\u306b\u304a\u3051\u308b\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u65b0\u6642\u4ee3\u300d\uff1a\u7ffb\u8a33<\/a><ul><li><a href=\"#e382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388e6a49ce8a8bce381aee696b0e69982e4bba3e3818ce382abe383abe38380e3838ee381ab-9\">\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u65b0\u6642\u4ee3\u304c\u30ab\u30eb\u30c0\u30ce\u306b\u5230\u6765<\/a><\/li><li><a href=\"#e381aae3819ce38193e381aee38384e383bce383abe3818ce382b2e383bce383a0e38381e382a7e383b3e382b8e383a3e383bce381aae381aee3818befbc9f-10\">\u306a\u305c\u3053\u306e\u30c4\u30fc\u30eb\u304c\u30b2\u30fc\u30e0\u30c1\u30a7\u30f3\u30b8\u30e3\u30fc\u306a\u306e\u304b\uff1f<\/a><\/li><li><a href=\"#e381aae3819ce5bda2e5bc8fe79a84e6a49ce8a8bce3818ce5bf85e8a681e381aae381aee3818befbc9f-11\">\u306a\u305c\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5fc5\u8981\u306a\u306e\u304b\uff1f<\/a><\/li><li><a href=\"#e7a781e3819fe381a1e381aee79baee68c87e38199e38282e381ae-12\">\u79c1\u305f\u3061\u306e\u76ee\u6307\u3059\u3082\u306e<\/a><\/li><li><a href=\"#e9968be799bae78ab6e6b381-13\">\u958b\u767a\u72b6\u6cc1<\/a><\/li><li><a href=\"#e382b7e383b3e38397e383abe381aae4bdbfe794a8e4be8b-14\">\u30b7\u30f3\u30d7\u30eb\u306a\u4f7f\u7528\u4f8b<\/a><ul><li><a href=\"#1-containskey-15\">1.&nbsp;containsKey<\/a><\/li><li><a href=\"#2-timehaselapsed-16\">2.&nbsp;timeHasElapsed<\/a><\/li><\/ul><\/li><li><a href=\"#e69c9fe5be85e38195e3828ce3828be58b95e4bd9ce381aee6a49ce8a8bc-17\">\u671f\u5f85\u3055\u308c\u308b\u52d5\u4f5c\u306e\u691c\u8a3c<\/a><\/li><li><a href=\"#smte382bde383abe38390e383bce381aee7b590e69e9cefbc9ae5ae9ae79086e381afe581bdefbc81-18\">SMT\u30bd\u30eb\u30d0\u30fc\u306e\u7d50\u679c\uff1a\u5b9a\u7406\u306f\u507d\uff01<\/a><\/li><li><a href=\"#e4bb8ae5be8ce381aee5b195e69c9b-19\">\u4eca\u5f8c\u306e\u5c55\u671b<\/a><\/li><\/ul><\/div><h3 class=\"wp-block-heading deb-block deb-block-e8d88ca\" id=\"e382abe383abe38380e3838ee381abe8a8aae3828ce3828be696b0e69982e4bba3efbc9ae382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388-1\"><strong>\u30ab\u30eb\u30c0\u30ce\u306b\u8a2a\u308c\u308b\u65b0\u6642\u4ee3\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u5b8c\u5168\u81ea\u52d5\u5316\u3078<\/strong><\/h3>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-239e4b9\" id=\"lean4e381a8z3e3818ce58887e3828ae68b93e3818fe38081e9968be799bae88085e38395e383ace383b3e38389e383aae383bce381aae38395e382a9e383bce3839e-2\"><strong>Lean4\u3068Z3\u304c\u5207\u308a\u62d3\u304f\u3001\u958b\u767a\u8005\u30d5\u30ec\u30f3\u30c9\u30ea\u30fc\u306a\u30d5\u30a9\u30fc\u30de\u30eb\u30fb\u30d9\u30ea\u30d5\u30a3\u30b1\u30fc\u30b7\u30e7\u30f3<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-f9c9a3e\">2025\u5e747\u670817\u65e5\u3001IOG\uff08Input Output Global\uff09\u306f\u3001\u30ab\u30eb\u30c0\u30ce\u306b\u304a\u3051\u308b\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u5b89\u5168\u6027\u3068\u4fe1\u983c\u6027\u3092\u98db\u8e8d\u7684\u306b\u9ad8\u3081\u308b\u65b0\u30c4\u30fc\u30eb\u306e\u958b\u767a\u3092<a href=\"https:\/\/iohk.io\/en\/blog\/posts\/2025\/07\/17\/a-new-era-of-smart-contract-verification-on-cardano\/\" data-type=\"link\" data-id=\"https:\/\/iohk.io\/en\/blog\/posts\/2025\/07\/17\/a-new-era-of-smart-contract-verification-on-cardano\/\">\u516c\u8868<\/a>\u3057\u307e\u3057\u305f\u3002\u3053\u306e\u30c4\u30fc\u30eb\u306f\u3001<strong>\u958b\u767a\u8005\u306e\u624b\u3092\u7169\u308f\u305b\u308b\u3053\u3068\u306a\u304f\u3001\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u300c\u5f62\u5f0f\u7684\u691c\u8a3c\uff08formal verification\uff09\u300d\u3092\u5b8c\u5168\u81ea\u52d5\u3067\u5b9f\u884c<\/strong>\u3067\u304d\u308b\u753b\u671f\u7684\u306a\u3082\u306e\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-be53e58\" id=\"e381aae3819ce5bda2e5bc8fe79a84e6a49ce8a8bce3818ce5bf85e8a681e381aae381aee3818befbc9f-3\"><strong>\u306a\u305c\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5fc5\u8981\u306a\u306e\u304b\uff1f<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-94b8cb2\">\u30ab\u30eb\u30c0\u30ce\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306f\u3001Plinth\u3001Aiken\u3001Plu-ts\u306a\u3069\u306e\u9ad8\u6c34\u6e96\u8a00\u8a9e\u3067\u8a18\u8ff0\u3055\u308c\u3001\u5b9f\u969b\u306e\u8cc7\u7523\u3092\u76f4\u63a5\u5236\u5fa1\u3057\u3066\u3044\u307e\u3059\u3002\u3064\u307e\u308a\u3001\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306b\u30d0\u30b0\u304c\u3042\u308c\u3070\u3001\u8cc7\u91d1\u304c\u76d7\u307e\u308c\u305f\u308a\u3001\u6c38\u4e45\u306b\u30ed\u30c3\u30af\u3055\u308c\u308b\u30ea\u30b9\u30af\u304c\u3042\u308a\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-4f3cc23\">\u5f93\u6765\u306e\u30c6\u30b9\u30c8\u3067\u306f\u3001\u60f3\u5b9a\u3057\u305f\u30b7\u30ca\u30ea\u30aa\u3057\u304b\u691c\u8a3c\u3067\u304d\u305a\u3001\u5b9f\u969b\u306b\u8d77\u3053\u308a\u3046\u308b\u3059\u3079\u3066\u306e\u6319\u52d5\u3092\u7db2\u7f85\u3059\u308b\u306e\u306f\u4e0d\u53ef\u80fd\u3067\u3059\u3002\u3053\u308c\u306b\u5bfe\u3057\u3066\u5f62\u5f0f\u7684\u691c\u8a3c\u306f\u3001\u300c\u3053\u306e\u6027\u8cea\u306f\u5e38\u306b\u6210\u308a\u7acb\u3064\u300d\u3068\u3044\u3046\u547d\u984c\u3092\u6570\u5b66\u7684\u306b\u8a3c\u660e\u3057\u3001<strong>\u3042\u3089\u3086\u308b\u72b6\u6cc1\u3067\u6b63\u3057\u304f\u52d5\u4f5c\u3059\u308b\u3053\u3068\u3092\u4fdd\u8a3c<\/strong>\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-11d1c7d\" id=\"e382b2e383bce383a0e38381e382a7e383b3e382b8e383a3e383bcefbc9alean4efbc8bz3e381abe38288e3828be5ae8ce585a8e887aae58b95e58c96-4\"><strong>\u30b2\u30fc\u30e0\u30c1\u30a7\u30f3\u30b8\u30e3\u30fc\uff1aLean4\uff0bZ3\u306b\u3088\u308b\u5b8c\u5168\u81ea\u52d5\u5316<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-f3977aa\">IOG\u306e\u65b0\u30c4\u30fc\u30eb\u306e\u6700\u5927\u306e\u7279\u9577\u306f\u3001<strong>\u958b\u767a\u8005\u304c\u8a3c\u660e\u3092\u66f8\u304f\u5fc5\u8981\u304c\u4e00\u5207\u306a\u3044\u5b8c\u5168\u81ea\u52d5\u5316<\/strong>\u3067\u3059\u3002Lean4\u3068\u3044\u3046\u8a3c\u660e\u8a00\u8a9e\u3068\u3001Z3\u3084CVC5\u3068\u3044\u3063\u305fSMT\u30bd\u30eb\u30d0\u30fc\u3092\u7d44\u307f\u5408\u308f\u305b\u308b\u3053\u3068\u3067\u3001\u6b21\u306e\u3088\u3046\u306a\u30d7\u30ed\u30bb\u30b9\u3092\u5b9f\u73fe\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-56439c0\">\n<li class=\"\">\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u3092\u5185\u90e8\u3067Lean4\u8868\u73fe\u306b\u81ea\u52d5\u5909\u63db<\/li>\n\n\n\n<li class=\"\">Universal Annotation Language\u3067\u30d7\u30ed\u30d1\u30c6\u30a3\uff08\u6027\u8cea\uff09\u3092\u6307\u5b9a<\/li>\n\n\n\n<li class=\"\">SMT\u30af\u30a8\u30ea\u306b\u5909\u63db\u3057\u3001\u5b9a\u7406\u3092\u8a3c\u660e or \u53cd\u4f8b\u3092\u63d0\u793a<\/li>\n\n\n\n<li class=\"\">\u554f\u984c\u304c\u3042\u308c\u3070\u30ea\u30d7\u30ec\u30a4\u53ef\u80fd\u306a\u5177\u4f53\u7684\u306a\u53cd\u4f8b\u3092\u8fd4\u5374<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-43f1214\">\u3064\u307e\u308a\u3001<strong>\u30dc\u30bf\u30f3\u4e00\u3064\u3067\u3001CI\/CD\u30d1\u30a4\u30d7\u30e9\u30a4\u30f3\u306b\u7d44\u307f\u8fbc\u3093\u3060\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u53ef\u80fd<\/strong>\u306b\u306a\u308a\u307e\u3059\u3002\u3057\u304b\u3082\u3001\u958b\u767a\u8005\u304c\u4f7f\u3044\u6163\u308c\u305f\u8a00\u8a9e\u3084\u6a5f\u80fd\u3092\u5236\u9650\u3057\u307e\u305b\u3093\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-7e3989a\" id=\"e6a49ce8a8bce4be8befbc9ae38399e382b9e38386e382a3e383b3e382b0e382b3e383b3e38388e383a9e382afe38388e381aee890bde381a8e38197e7a9b4-5\"><strong>\u691c\u8a3c\u4f8b\uff1a\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u843d\u3068\u3057\u7a74<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-4aef0b7\">\u8a18\u4e8b\u3067\u306f\u3001VacuumLabs\u306eCTF\u304b\u3089\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\uff08\u6a29\u5229\u78ba\u5b9a\uff09\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u4f8b\u3092\u7d39\u4ecb\u3002\u672c\u6765\u306f\u300c\u6307\u5b9a\u3055\u308c\u305f\u6642\u523b\u4ee5\u964d\u306b\u3001\u53d7\u76ca\u8005\u672c\u4eba\u304c\u7f72\u540d\u3059\u308c\u3070\u8cc7\u91d1\u3092\u5f15\u304d\u51fa\u305b\u308b\u300d\u3068\u3044\u3046\u4ed5\u69d8\u3067\u3059\u304c\u3001<strong>\u5b9f\u88c5\u306b\u6f5c\u3080\u30ed\u30b8\u30c3\u30af\u306e\u7518\u3055<\/strong>\u3092\u30c4\u30fc\u30eb\u304c\u898b\u629c\u304d\u307e\u3057\u305f\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-bd4cc87\">\u4f8b\u3068\u3057\u3066\u3001validity_range\u306e\u4e0a\u9650\u3092\u975e\u5e38\u306b\u5927\u304d\u304f\u8a2d\u5b9a\u3059\u308b\u3068\u3001\u307e\u3060\u6642\u9593\u304c\u7d4c\u3063\u3066\u3044\u306a\u3044\u306e\u306b\u8cc7\u91d1\u304c\u5f15\u304d\u51fa\u305b\u3066\u3057\u307e\u3046\u3068\u3044\u3046\u91cd\u5927\u306a\u30d0\u30b0\u304c\u691c\u51fa\u3055\u308c\u307e\u3057\u305f\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-8b01d75\">\u3053\u308c\u306f\u3001<strong>\u5f62\u5f0f\u7684\u691c\u8a3c\u306a\u3057\u3067\u306f\u767a\u898b\u304c\u56f0\u96e3\u306a\u5883\u754c\u30b1\u30fc\u30b9<\/strong>\u3067\u3042\u308a\u3001\u3053\u306e\u3088\u3046\u306a\u76f2\u70b9\u3092SMT\u30bd\u30eb\u30d0\u30fc\u304c\u81ea\u52d5\u7684\u306b\u53cd\u4f8b\u3068\u3057\u3066\u63d0\u793a\u3057\u3066\u304f\u308c\u308b\u306e\u306f\u5f37\u529b\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-d182b2b\" id=\"e9968be799bae78ab6e6b381e381a8e4bb8ae5be8ce381aee5b195e69c9b-6\"><strong>\u958b\u767a\u72b6\u6cc1\u3068\u4eca\u5f8c\u306e\u5c55\u671b<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-601e7f8\">\u3053\u306e\u30c4\u30fc\u30eb\u306f\u73fe\u5728\u3001Lean4\u306e\u63a8\u8ad6\u30b3\u30a2\u3068SMT\u30d0\u30c3\u30af\u30a8\u30f3\u30c9\u306e\u63a5\u7d9a\u307e\u3067\u5b8c\u6210\u3057\u3066\u304a\u308a\u3001\u4eca\u5f8c\u306f\u4ee5\u4e0b\u3092\u76ee\u6307\u3057\u307e\u3059\uff1a<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-612e1b5\">\n<li class=\"\">UPLC\u30b3\u30fc\u30c9\uff08\u4f4e\u30ec\u30d9\u30eb\u8a00\u8a9e\uff09\u3078\u306e\u5bfe\u5fdc<\/li>\n\n\n\n<li class=\"\">Plutus Core\u3068CEK\u30de\u30b7\u30f3\u306e\u518d\u5b9f\u88c5\u306b\u3088\u308b\u4f4e\u5c64\u691c\u8a3c\u306e\u81ea\u52d5\u5316<\/li>\n\n\n\n<li class=\"\">\u6700\u9069\u5316\u30b3\u30fc\u30c9\u306b\u5bfe\u3059\u308b\u5f62\u5f0f\u7684\u8a3c\u660e\u306e\u652f\u63f4<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-583c47d\">\u6b21\u56de\u8a18\u4e8b\u3067\u306f\u3001UPLC\u30ec\u30d9\u30eb\u306e\u81ea\u52d5\u691c\u8a3c\u306e\u5177\u4f53\u4f8b\u304c\u7d39\u4ecb\u3055\u308c\u308b\u4e88\u5b9a\u3067\u3059\u3002<\/p>\n\n\n\n<hr class=\"wp-block-separator has-alpha-channel-opacity\"\/>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-09aad8a\" id=\"e381bee381a8e38281efbc9ae382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388e381aee69caae69da5e381afe3808ce8a8bce6988ee58faf-7\"><strong>\u307e\u3068\u3081\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u672a\u6765\u306f\u300c\u8a3c\u660e\u53ef\u80fd\u306a\u5b89\u5168\u6027\u300d\u3078<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-ca65ba2\">\u3053\u306e\u81ea\u52d5\u691c\u8a3c\u30c4\u30fc\u30eb\u306f\u3001\u30ab\u30eb\u30c0\u30ce\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306b\u5bfe\u3057\u3066\u6b21\u306e\u3088\u3046\u306a\u672a\u6765\u3092\u3082\u305f\u3089\u3057\u307e\u3059\uff1a<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-88dd4d9\">\n<li class=\"\">\u8ab0\u3067\u3082\u7c21\u5358\u306b\u30bb\u30ad\u30e5\u30a2\u306a\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u3092\u958b\u767a\u53ef\u80fd<\/li>\n\n\n\n<li class=\"\">\u610f\u56f3\u3057\u306a\u3044\u52d5\u4f5c\u3092\u4e8b\u524d\u306b\u6392\u9664<\/li>\n\n\n\n<li class=\"\">\u30ac\u30d0\u30ca\u30f3\u30b9\u63d0\u6848\u3084DeFi\u5951\u7d04\u306e\u900f\u660e\u6027\u30fb\u4fe1\u983c\u6027\u3092\u62c5\u4fdd<\/li>\n\n\n\n<li class=\"\">Cardano\u4e0a\u3067\u306e\u30a8\u30f3\u30bf\u30fc\u30d7\u30e9\u30a4\u30ba\u5229\u7528\u3084\u898f\u5236\u5bfe\u5fdc\u306b\u3082\u5927\u304d\u306a\u524d\u9032<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-335bb6c\">\u307e\u3055\u306b\u3001<strong>\u30ab\u30eb\u30c0\u30ce\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306b\u300c\u81ea\u52d5\u3067\u5b89\u5168\u3092\u8a3c\u660e\u3059\u308b\u300d\u3068\u3044\u3046\u65b0\u3057\u3044\u30d1\u30e9\u30c0\u30a4\u30e0<\/strong>\u304c\u5230\u6765\u3057\u305f\u3068\u3044\u3048\u308b\u3067\u3057\u3087\u3046\u3002<\/p>\n\n\n\n<hr class=\"wp-block-separator has-alpha-channel-opacity\"\/>\n\n\n\n<p class=\"deb-block deb-block-8c92e0e\"><a class=\"\" href=\"https:\/\/iohk.io\/en\/blog\/posts\/2025\/07\/17\/a-new-era-of-smart-contract-verification-on-cardano\/\"><\/a>\u4ee5\u4e0b\u306fIOG\u30d6\u30ed\u30b0\u8a18\u4e8b\u300c<a class=\"\" href=\"https:\/\/iohk.io\/en\/blog\/posts\/2025\/07\/17\/a-new-era-of-smart-contract-verification-on-cardano\/\">A new era of smart contract verification on Cardano<\/a>\u300d\u3092\u7ffb\u8a33\u3057\u305f\u3082\u306e\u3067\u3059\u3002<\/p>\n\n\n\n<h3 class=\"wp-block-heading deb-block deb-block-f5770ff\" id=\"ioge38396e383ade382b0e3808ce382abe383abe38380e3838ee381abe3818ae38191e3828be382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382af-8\">IOG\u30d6\u30ed\u30b0\u300c<strong>\u30ab\u30eb\u30c0\u30ce\u306b\u304a\u3051\u308b\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u65b0\u6642\u4ee3<\/strong>\u300d\uff1a\u7ffb\u8a33<\/h3>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full has-custom-border deb-block deb-block-955a3e0\"><img loading=\"lazy\" decoding=\"async\" width=\"800\" height=\"450\" src=\"https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp\" alt=\"\" class=\"has-border-color has-aaaaaa-border-color wp-image-42330\" srcset=\"https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp 800w, https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-300x169.webp 300w, https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-768x432.webp 768w, https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-450x253.webp 450w\" sizes=\"auto, (max-width: 800px) 100vw, 800px\" \/><\/figure>\n<\/div>\n\n\n<p class=\"deb-block deb-block-9e4e87a\"><strong>\u30bb\u30ad\u30e5\u30ea\u30c6\u30a3\u306f\u91cd\u8981\u3067\u3059\u3002\u30ab\u30eb\u30c0\u30ce\u306e\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u5f62\u5f0f\u7684\u691c\u8a3c\uff08\u30d5\u30a9\u30fc\u30de\u30eb\u30fb\u30d9\u30ea\u30d5\u30a3\u30b1\u30fc\u30b7\u30e7\u30f3\uff09\u3092\u3053\u308c\u307e\u3067\u4ee5\u4e0a\u306b\u7c21\u5358\u306b\u3001\u8fc5\u901f\u306b\u3001\u305d\u3057\u3066\u624b\u8efd\u306b\u884c\u3048\u308b\u65b0\u30c4\u30fc\u30eb\u306e\u767b\u5834\u306b\u3064\u3044\u3066\u3054\u7d39\u4ecb\u3057\u307e\u3059\u3002<\/strong><\/p>\n\n\n\n<p class=\"deb-block deb-block-03b0398\">2025\u5e747\u670817\u65e5\u3000\u8457\u8005\uff1aRomain Soulat<\/p>\n\n\n\n<hr class=\"wp-block-separator has-alpha-channel-opacity\"\/>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-c5e1475\" id=\"e382b9e3839ee383bce38388e382b3e383b3e38388e383a9e382afe38388e6a49ce8a8bce381aee696b0e69982e4bba3e3818ce382abe383abe38380e3838ee381ab-9\"><strong>\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u65b0\u6642\u4ee3\u304c\u30ab\u30eb\u30c0\u30ce\u306b\u5230\u6765<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-4841ac6\">\u30ab\u30eb\u30c0\u30ce\u4e0a\u3067\u306f\u3001\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306f Plinth\u3001Aiken\u3001Plu-ts \u3068\u3044\u3063\u305f\u5f37\u529b\u306a\u9ad8\u6c34\u6e96\u8a00\u8a9e\u3067\u8a18\u8ff0\u3055\u308c\u307e\u3059\u3002\u3053\u308c\u3089\u306e\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306f\u5b9f\u969b\u306e\u4fa1\u5024\u3042\u308b\u8cc7\u7523\u3092\u5236\u5fa1\u3057\u3066\u3044\u307e\u3059\u3002\u305d\u306e\u305f\u3081\u3001\u3082\u3057\u30d0\u30b0\u304c\u3042\u308c\u3070\u3001\u8cc7\u91d1\u304c\u76d7\u307e\u308c\u305f\u308a\u3001\u6c38\u4e45\u306b\u30ed\u30c3\u30af\u3055\u308c\u308b\u6050\u308c\u304c\u3042\u308a\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-6413232\">Input Output\uff08IO\uff09\u306f\u3001\u30ab\u30eb\u30c0\u30ce\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306b\u5f62\u5f0f\u7684\u691c\u8a3c\u3092\u5c0e\u5165\u3059\u308b\u305f\u3081\u306e\u65b0\u3057\u3044\u30c4\u30fc\u30eb\u3092\u958b\u767a\u4e2d\u3067\u3059\u3002\u30a8\u30b3\u30b7\u30b9\u30c6\u30e0\u5185\u306b\u306f Agda \u3084 Rocq\uff08\u65e7 Coq\uff09\u306a\u3069\u306e\u8a3c\u660e\u652f\u63f4\u30c4\u30fc\u30eb\u3092\u30d9\u30fc\u30b9\u3068\u3057\u305f\u65e2\u5b58\u30c4\u30fc\u30eb\u304c\u3042\u308a\u3001\u9ad8\u3044\u4fdd\u8a3c\u3092\u63d0\u4f9b\u3057\u3066\u3044\u307e\u3059\u304c\u3001\u3053\u308c\u3089\u306e\u4f7f\u7528\u306b\u306f\u5c02\u9580\u77e5\u8b58\u304c\u5fc5\u8981\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-76f093d\">\u4eca\u56de\u306e\u65b0\u30c4\u30fc\u30eb\u306f\u3001Lean4\u3068\u3044\u3046\u8a3c\u660e\u30b7\u30b9\u30c6\u30e0\u3068\u3001Z3\u306e\u3088\u3046\u306aSMT\u30bd\u30eb\u30d0\u30fc\uff08\u5b9a\u7406\u81ea\u52d5\u8a3c\u660e\u5668\uff09\u306e\u529b\u3092\u7d44\u307f\u5408\u308f\u305b\u3001\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u304c\u610f\u56f3\u901a\u308a\u306b\u52d5\u4f5c\u3059\u308b\u3053\u3068\u3092\u81ea\u52d5\u7684\u306b\u30c1\u30a7\u30c3\u30af\u3057\u307e\u3059\u3002\u76ee\u6a19\u306f\u3001\u958b\u767a\u8005\u304c\u81ea\u3089\u8a3c\u660e\u3092\u66f8\u304f\u5fc5\u8981\u3092\u306a\u304f\u3059\u3053\u3068\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-b0bf4d0\">\u4ee5\u4e0b\u306f\u7d9a\u304d\u306e\u30bb\u30af\u30b7\u30e7\u30f3\u306e\u7ffb\u8a33\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-d1c676b\" id=\"e381aae3819ce38193e381aee38384e383bce383abe3818ce382b2e383bce383a0e38381e382a7e383b3e382b8e383a3e383bce381aae381aee3818befbc9f-10\"><strong>\u306a\u305c\u3053\u306e\u30c4\u30fc\u30eb\u304c\u30b2\u30fc\u30e0\u30c1\u30a7\u30f3\u30b8\u30e3\u30fc\u306a\u306e\u304b\uff1f<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-e5a72ac\">\u3053\u306e\u30c4\u30fc\u30eb\u304c\u753b\u671f\u7684\u306a\u306e\u306f\u3001\u5b8c\u5168\u81ea\u52d5\u5316\u3055\u308c\u3066\u3044\u308b\u70b9\u306b\u3042\u308a\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-5e7248b\">\u624b\u52d5\u3067\u306e\u8a3c\u660e\u4f5c\u6210\u3084\u5c02\u9580\u5bb6\u306b\u3088\u308b\u4ecb\u5165\u306f\u4e00\u5207\u4e0d\u8981\u3067\u3059\u3002\u30dc\u30bf\u30f3\u3092\u30af\u30ea\u30c3\u30af\u3059\u308b\u3060\u3051\u3067\u3001\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5b8c\u4e86\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-bdb0b71\">\u3064\u307e\u308a\u3001\u3053\u306e\u30c4\u30fc\u30eb\u306fCI\/CD\u30d1\u30a4\u30d7\u30e9\u30a4\u30f3\u306b\u76f4\u63a5\u7d71\u5408\u3067\u304d\u3001\u30b3\u30df\u30c3\u30c8\u306e\u305f\u3073\u306b\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u5f62\u5f0f\u7684\u691c\u8a3c\u3092\u5373\u5ea7\u306b\u3001\u7d99\u7d9a\u7684\u306b\u3001\u305d\u3057\u3066\u624b\u9803\u306a\u30b3\u30b9\u30c8\u3067\u884c\u3048\u308b\u306e\u3067\u3059\u3002\u73fe\u5728\u3082\u958b\u767a\u4e2d\u3067\u3042\u308a\u3001\u4eca\u5f8c\u63d0\u4f9b\u304c\u4e88\u5b9a\u3055\u308c\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-a073830\" id=\"e381aae3819ce5bda2e5bc8fe79a84e6a49ce8a8bce3818ce5bf85e8a681e381aae381aee3818befbc9f-11\"><strong>\u306a\u305c\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5fc5\u8981\u306a\u306e\u304b\uff1f<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-38f2aeb\">\u30c6\u30b9\u30c8\u3067\u306f\u3001\u958b\u767a\u8005\u304c\u601d\u3044\u3064\u3044\u305f\u30b1\u30fc\u30b9\u3084\u30b7\u30ca\u30ea\u30aa\u3057\u304b\u691c\u8a3c\u3067\u304d\u307e\u305b\u3093\u3002\u30d7\u30ed\u30d1\u30c6\u30a3\u30d9\u30fc\u30b9\u306e\u30c6\u30b9\u30c8\uff08\u7279\u6027\u30d9\u30fc\u30b9\u30c6\u30b9\u30c8\uff09\u306f\u3053\u308c\u3092\u88dc\u5b8c\u3057\u307e\u3059\u304c\u3001\u305d\u308c\u3067\u3082\u5927\u90e8\u5206\u306e\u30c6\u30b9\u30c8\u7a7a\u9593\u306f\u672a\u691c\u8a3c\u306e\u307e\u307e\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-9fad905\">\u52a0\u3048\u3066\u3001\u5305\u62ec\u7684\u306a\u30c6\u30b9\u30c8\u30b9\u30a4\u30fc\u30c8\u3092\u69cb\u7bc9\u3059\u308b\u306b\u306f\u3001\u591a\u304f\u306e\u30b7\u30ca\u30ea\u30aa\u3068\u653b\u6483\u30d1\u30bf\u30fc\u30f3\u3092\u7db2\u7f85\u3059\u308b\u5fc5\u8981\u304c\u3042\u308a\u3001\u958b\u767a\u306b\u591a\u5927\u306a\u52b4\u529b\u304c\u304b\u304b\u308a\u307e\u3059\u3002\u30c6\u30b9\u30c8\u5bfe\u8c61\u304c\u591a\u304f\u8907\u96d1\u3067\u3042\u308b\u307b\u3069\u3001\u4fdd\u5b88\u3082\u56f0\u96e3\u306b\u306a\u308a\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-e818ae6\">\u5f62\u5f0f\u7684\u691c\u8a3c\u3067\u306f\u3001\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u7279\u6027\uff08\u30d7\u30ed\u30d1\u30c6\u30a3\uff09\u3092\u660e\u793a\u7684\u306b\u8a18\u8ff0\u3057\u3001\u305d\u308c\u304c\u5e38\u306b\u6210\u308a\u7acb\u3064\u3053\u3068\u3092\u6570\u5b66\u7684\u306b\u8a3c\u660e\u3067\u304d\u307e\u3059\u3002\u4e00\u90e8\u306e\u5f62\u5f0f\u7684\u691c\u8a3c\u6280\u8853\u3067\u306f\u3001\u7279\u6027\u304c\u6210\u308a\u7acb\u305f\u306a\u3044\u5834\u5408\u306b\u53cd\u4f8b\uff08\u30ab\u30a6\u30f3\u30bf\u30fc\u30a8\u30b0\u30b6\u30f3\u30d7\u30eb\uff09\u3092\u751f\u6210\u3067\u304d\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-eb74806\">\u65e2\u5b58\u306e\u5f62\u5f0f\u7684\u691c\u8a3c\u30c4\u30fc\u30eb\u306f\u3001\u9ad8\u5ea6\u306a\u30bb\u30ad\u30e5\u30ea\u30c6\u30a3\u4fdd\u8a3c\u3092\u63d0\u4f9b\u3059\u308b\u4e00\u65b9\u3067\u3001\u5225\u306e\u8a00\u8a9e\u3067\u30e2\u30c7\u30eb\u3092\u958b\u767a\u3057\u306a\u3051\u308c\u3070\u306a\u3089\u306a\u3044\u4e0a\u306b\u3001\u7279\u6b8a\u306a\u5c02\u9580\u77e5\u8b58\u304c\u5fc5\u8981\u3067\u3059\u3002\u305d\u306e\u8907\u96d1\u3055\u3001\u81ea\u52d5\u5316\u306e\u6b20\u5982\u3001\u518d\u5229\u7528\u53ef\u80fd\u306a\u53cd\u4f8b\u304c\u751f\u6210\u3067\u304d\u306a\u3044\u3068\u3044\u3046\u70b9\u304b\u3089\u3001\u307b\u3068\u3093\u3069\u306e\u958b\u767a\u8005\u306b\u3068\u3063\u3066\u306f\u6577\u5c45\u304c\u9ad8\u3044\u306e\u304c\u73fe\u72b6\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-32cc55e\" id=\"e7a781e3819fe381a1e381aee79baee68c87e38199e38282e381ae-12\"><strong>\u79c1\u305f\u3061\u306e\u76ee\u6307\u3059\u3082\u306e<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-49025bb\">IO\u304c\u958b\u767a\u4e2d\u306e\u81ea\u52d5\u5f62\u5f0f\u691c\u8a3c\u30c4\u30fc\u30eb\u306f\u3001\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u3092\u4ee5\u4e0b\u306e\u624b\u9806\u3067\u691c\u8a3c\u3059\u308b\u3053\u3068\u3092\u76ee\u6307\u3057\u3066\u3044\u307e\u3059\uff1a<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-09495b8\">\n<li class=\"\">\u8868\u5c64\u306e\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\u8a00\u8a9e\uff08Plinth\u3001Aiken\u3001Plu-ts\u3001UPLC\u306a\u3069\uff09\u304b\u3089\u3001Lean4\u3067\u306e\u5185\u90e8\u8868\u73fe\u306b\u81ea\u52d5\u3067\u5909\u63db\u3057\u3001\u610f\u5473\u7684\u306b\u5fe0\u5b9f\u306a\u30e2\u30c7\u30eb\u3092\u69cb\u7bc9\u3002<\/li>\n\n\n\n<li class=\"\">\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u7279\u6027\u3092\u3001Lean\u306e\u5b9a\u7406\u3068\u3057\u3066\u8a18\u8ff0\u3002\u7279\u6027\u306f\u300cUniversal Annotation Language\uff08\u6c4e\u7528\u30a2\u30ce\u30c6\u30fc\u30b7\u30e7\u30f3\u8a00\u8a9e\uff09\u300d\u3067\u6307\u5b9a\u3057\u3001\u8a00\u8a9e\u9593\u3092\u8d85\u3048\u3066\u5229\u7528\u53ef\u80fd\u306b\u3002<\/li>\n\n\n\n<li class=\"\">Lean\u8868\u73fe\u3068\u5b9a\u7406\u3092\u3001\u7b49\u4fa1\u3060\u304cSMT\u30bd\u30eb\u30d0\u30fc\u3067\u6271\u3048\u308b\u5f62\u306b\u5909\u63db\u30fb\u7c21\u7565\u5316\u3002<\/li>\n\n\n\n<li class=\"\">\u3053\u308c\u3089\u3092Z3\u3084CVC5\u3068\u3044\u3063\u305f\u5f37\u529b\u306aSMT\u30bd\u30eb\u30d0\u30fc\u306b\u6e21\u3059\u3002<\/li>\n\n\n\n<li class=\"\">\u7d50\u679c\u3068\u3057\u3066\u4ee5\u4e0b\u306e\u3044\u305a\u308c\u304b\u3092\u8fd4\u3059\uff1a\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-970442d\">\n<li class=\"\">\u7279\u6027\u304c\u6210\u308a\u7acb\u3064\u3068\u3044\u3046\u30ea\u30d7\u30ec\u30a4\u53ef\u80fd\u306a\u8a3c\u660e<\/li>\n\n\n\n<li class=\"\">\u554f\u984c\u3092\u5f15\u304d\u8d77\u3053\u3059\u5177\u4f53\u7684\u306a\u5b9f\u884c\u30c8\u30ec\u30fc\u30b9\u3092\u542b\u3093\u3060\u30ea\u30d7\u30ec\u30a4\u53ef\u80fd\u306a\u53cd\u4f8b<\/li>\n\n\n\n<li class=\"\">\u30bd\u30eb\u30d0\u30fc\u304c\u5224\u5b9a\u3067\u304d\u306a\u304b\u3063\u305f\u5834\u5408\u306f\u3001\u5c02\u9580\u5bb6\u306b\u3088\u308b\u624b\u52d5\u89e3\u6c7a\u7528\u306e\u8a3c\u660e\u8ab2\u984c\uff08proof obligation\uff09<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-190e5bf\">\u3053\u306e\u30c4\u30fc\u30eb\u306f\u3001\u5185\u90e8\u306b\u9ad8\u5ea6\u306a\u6700\u9069\u5316\u30fb\u5358\u7d14\u5316\u51e6\u7406\u3068Cardano\u7279\u6709\u306e\u77e5\u898b\u3092\u7d44\u307f\u8fbc\u3080\u3053\u3068\u3067\u3001\u5c02\u9580\u5bb6\u306e\u4ecb\u5165\u3092\u6975\u529b\u6e1b\u3089\u3059\u8a2d\u8a08\u306b\u306a\u3063\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-3ff5f2e\">\u4ee5\u4e0b\u306f\u7d9a\u304d\u306e\u30bb\u30af\u30b7\u30e7\u30f3\u300c\u958b\u767a\u72b6\u6cc1\u300d\u306e\u65e5\u672c\u8a9e\u8a33\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-674ab2a\" id=\"e9968be799bae78ab6e6b381-13\"><strong>\u958b\u767a\u72b6\u6cc1<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-7b138f0\">\u73fe\u5728\u3001\u3053\u306e\u30c4\u30fc\u30eb\u306e\u300c\u63a8\u8ad6\u30b3\u30a2\uff08reasoning core\uff09\u300d\u306f\u5f37\u529b\u306a\u30d0\u30fc\u30b8\u30e7\u30f3\u304c\u5b8c\u6210\u3057\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-02db6d3\">\u975e\u5e38\u306b\u5c02\u9580\u7684\u306a\u6700\u9069\u5316\u30fb\u7c21\u7565\u5316\u30fb\u6b63\u898f\u5316\u306e\u66f8\u304d\u63db\u3048\u30eb\u30fc\u30eb\u304c\u591a\u6570\u5b9f\u88c5\u3055\u308c\u3066\u304a\u308a\u3001\u73fe\u5b9f\u7684\u306aCardano\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u95a2\u6570\u306b\u3082\u30b9\u30b1\u30fc\u30e9\u30d6\u30eb\u306b\u5bfe\u5fdc\u3067\u304d\u308b\u3053\u3068\u304c\u5b9f\u8a3c\u3055\u308c\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-39c2ce4\">\u307e\u305f\u3001Plinth\u3084Aiken\u306a\u3069\u306e\u8868\u5c64\u8a00\u8a9e\u304c\u63d0\u4f9b\u3059\u308b\u9ad8\u6c34\u6e96\u306a\u6a5f\u80fd\u306e\u591a\u304f\u3092\u8003\u616e\u3057\u3066\u3044\u308b\u305f\u3081\u3001\u958b\u767a\u8005\u304c\u3053\u308c\u3089\u306e\u8a00\u8a9e\u3067\u4f7f\u3044\u6163\u308c\u305f\u6a5f\u80fd\u3092\u5236\u9650\u3055\u308c\u308b\u3053\u3068\u306a\u304f\u3001\u5f53\u30c4\u30fc\u30eb\u3092\u6d3b\u7528\u3067\u304d\u308b\u3088\u3046\u306b\u8a2d\u8a08\u3055\u308c\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-426d86d\">Lean4\u306e\u5b9a\u7406\uff08\u30b4\u30fc\u30eb\uff09\u3092SMT\u30af\u30a8\u30ea\u3078\u3068\u5909\u63db\u3059\u308bSMT\u30d0\u30c3\u30af\u30a8\u30f3\u30c9\u3078\u306e\u30c8\u30e9\u30f3\u30b9\u30ec\u30fc\u30b7\u30e7\u30f3\u3082\u69cb\u7bc9\u6e08\u307f\u3067\u3001\u3055\u3089\u306b\u751f\u6210\u3055\u308c\u305f\u53cd\u4f8b\u3092Lean\u306b\u623b\u3059\u4ed5\u7d44\u307f\u3082\u5099\u3048\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-f5bf2aa\" id=\"e382b7e383b3e38397e383abe381aae4bdbfe794a8e4be8b-14\"><strong>\u30b7\u30f3\u30d7\u30eb\u306a\u4f7f\u7528\u4f8b<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-9c7b84e\">\u73fe\u5728\u3001\u307e\u3060\u3069\u306e\u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0\u8a00\u8a9e\u304b\u3089Lean4\u3078\u306e\u5b8c\u5168\u306a\u30c8\u30e9\u30f3\u30b9\u30d1\u30a4\u30e9\uff08\u81ea\u52d5\u5909\u63db\u5668\uff09\u306f\u5b58\u5728\u3057\u3066\u3044\u307e\u305b\u3093\u304c\u3001Lean4\u306e\u4f8b\u3092\u4f7f\u3063\u3066\u5f53\u30c4\u30fc\u30eb\u306e\u52d5\u4f5c\u3092\u5b9f\u6f14\u3067\u304d\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-22cd519\">\u3053\u3053\u3067\u306f\u3001VacuumLabs\u306e\u300c\u30ad\u30e3\u30d7\u30c1\u30e3\u30fb\u30b6\u30fb\u30d5\u30e9\u30c3\u30b0\uff08CTF\uff09\u300d\u30c1\u30e3\u30ec\u30f3\u30b8\u306b\u304a\u3051\u308b\u300c\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\uff08\u6a29\u5229\u78ba\u5b9a\uff09\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u300d\u306e\u4f8b\u3092\u624b\u52d5\u3067Lean4\u306b\u7ffb\u8a33\u3057\u305f\u3082\u306e\u3092\u4f7f\u7528\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-c5a1c2c\">\u4ee5\u4e0b\u306e\u30d0\u30ea\u30c7\u30fc\u30bf\uff08validator\uff09\u306f\u3001\u4ee5\u4e0b\u306e\u6761\u4ef6\u3092\u6e80\u305f\u3059\u3068\u304d\u306e\u307f\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\u30fb\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306b\u30ed\u30c3\u30af\u3055\u308c\u305f\u8cc7\u91d1\u3092\u4f7f\u7528\u53ef\u80fd\u3068\u3057\u307e\u3059\uff1a<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-c7c0de4\">\n<li class=\"\">\u30c8\u30e9\u30f3\u30b6\u30af\u30b7\u30e7\u30f3\u306b\u3001\u60f3\u5b9a\u3055\u308c\u305f\u53d7\u76ca\u8005\u306e\u7f72\u540d\u304c\u542b\u307e\u308c\u3066\u3044\u308b<\/li>\n\n\n\n<li class=\"\">\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\u671f\u9593\u304c\u3059\u3067\u306b\u7d4c\u904e\u3057\u3066\u3044\u308b<\/li>\n<\/ul>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-22e739b\"><code>def validator : Demo -&gt; VestingDatum -&gt; VestingRedeemer -&gt; ScriptContext -&gt; Bool :=\n    fun demo datum _ sc =&gt;\n        let transaction := sc.transaction;\n        let purpose := sc.purpose;\n        let signatories := transaction.signatories;\n        let v_range := transaction.validity_range\n        (purpose == Purpose.Spending) &amp;&amp; (containsKey signatories datum.beneficiary demo) &amp;&amp; (timeHasElapsed v_range datum.lock_until)<\/code><\/pre>\n\n\n\n<p class=\"deb-block deb-block-6340cd5\">\u3053\u3053\u3067\u306f2\u3064\u306e\u30d8\u30eb\u30d1\u30fc\u95a2\u6570\u304c\u4f7f\u7528\u3055\u308c\u3066\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<h5 class=\"wp-block-heading deb-block deb-block-4bdfd6e\" id=\"1-containskey-15\"><strong>1.&nbsp;containsKey<\/strong><\/h5>\n\n\n\n<p class=\"deb-block deb-block-f3b94bc\">\u3053\u306e\u95a2\u6570\u306f\u3001\u4e0e\u3048\u3089\u308c\u305f\u7f72\u540d\u30ea\u30b9\u30c8\u306b\u53d7\u76ca\u8005\u306e\u9375\u304c\u542b\u307e\u308c\u3066\u3044\u308b\u304b\u3069\u3046\u304b\u3092\u78ba\u8a8d\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-17d0a82\"><code>def containsKey : List VerificationKeyHash -&gt; VerificationKeyHash -&gt; Bool :=\n   fun keys key =&gt;\n   match keys with\n   | &#91;] =&gt; false\n   | k :: ks =&gt; if k == key then true else containsKey ks key<\/code><\/pre>\n\n\n\n<h5 class=\"wp-block-heading deb-block deb-block-4ce2ce7\" id=\"2-timehaselapsed-16\"><strong>2.&nbsp;timeHasElapsed<\/strong><\/h5>\n\n\n\n<p class=\"deb-block deb-block-99b0d71\">\u3053\u306e\u95a2\u6570\u306f\u3001\u6307\u5b9a\u3055\u308c\u305f\u30d9\u30b9\u30c6\u30a3\u30f3\u30b0\u6642\u9593\u304c\u7d4c\u904e\u3057\u3066\u3044\u308b\u304b\u3069\u3046\u304b\u3092\u30c1\u30a7\u30c3\u30af\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-8bb2167\"><code>def timeHasElapsed : ValidityRange -&gt; POSIXTime -&gt; Bool :=\n    fun range time =&gt;\n        range.upper_bound &gt;= time.time<\/code><\/pre>\n\n\n\n<p class=\"deb-block deb-block-7e24d15\">\u3053\u306e\u30b3\u30fc\u30c9\u306f\u3001\u958b\u767a\u8005\u304cPlu-ts\u3084Aiken\u3068\u3044\u3063\u305fCardano\u306e\u4efb\u610f\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u8a00\u8a9e\u3092\u4f7f\u3063\u3066\u8a18\u8ff0\u3057\u305f\u3067\u3042\u308d\u3046\u5185\u5bb9\u3068\u975e\u5e38\u306b\u8fd1\u3044\u3082\u306e\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-051a43e\">\u4ee5\u4e0b\u306f\u7d9a\u304d\u306e\u30bb\u30af\u30b7\u30e7\u30f3\u306e\u7ffb\u8a33\u3067\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-d799fb8\" id=\"e69c9fe5be85e38195e3828ce3828be58b95e4bd9ce381aee6a49ce8a8bc-17\"><strong>\u671f\u5f85\u3055\u308c\u308b\u52d5\u4f5c\u306e\u691c\u8a3c<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-e23cae1\">\u901a\u5e38\u3001\u3053\u3046\u3057\u305f\u30b3\u30fc\u30c9\u304c\u8981\u4ef6\u3092\u6e80\u305f\u3057\u3066\u3044\u308b\u304b\u3069\u3046\u304b\u3092\u78ba\u8a8d\u3059\u308b\u306b\u306f\u3001\u30c6\u30b9\u30bf\u30fc\uff08\u3042\u308b\u3044\u306f\u958b\u767a\u8005\u81ea\u8eab\uff09\u304c\u540d\u76ee\u30b1\u30fc\u30b9\u3084\u5883\u754c\u30b1\u30fc\u30b9\u3092\u542b\u3080\u8907\u6570\u306e\u30b7\u30ca\u30ea\u30aa\u3092\u624b\u52d5\u3067\u66f8\u304f\u5fc5\u8981\u304c\u3042\u308a\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-c6cb589\">\u3057\u304b\u3057\u79c1\u305f\u3061\u306e\u30a2\u30d7\u30ed\u30fc\u30c1\u3067\u306f\u3001\u671f\u5f85\u3055\u308c\u308b\u52d5\u4f5c\u3001\u3064\u307e\u308a\u300c\u6e80\u305f\u3059\u3079\u304d\u7279\u6027\uff08\u30d7\u30ed\u30d1\u30c6\u30a3\uff09\u300d\u3060\u3051\u3092\u8a18\u8ff0\u3059\u308c\u3070\u5341\u5206\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-e07ee59\">\u671f\u5f85\u3055\u308c\u308b\u52d5\u4f5c\u306fLean4\u306b\u304a\u3051\u308b\u5b9a\u7406\uff08theorem\uff09\u3068\u3057\u3066\u8868\u73fe\u3067\u304d\u307e\u3059\u3002\u73fe\u6bb5\u968e\u3067\u306f\u3001\u3053\u306e\u8a00\u8a9e\u306f\u3042\u307e\u308a\u30e6\u30fc\u30b6\u30fc\u30d5\u30ec\u30f3\u30c9\u30ea\u30fc\u3068\u306f\u8a00\u3048\u307e\u305b\u3093\u304c\uff08\u4eca\u5f8c\u6539\u5584\u4e88\u5b9a\u3067\u3059\uff01\uff09\u3001\u4ee5\u4e0b\u306e\u3088\u3046\u306b\u8a18\u8ff0\u3067\u304d\u307e\u3059\uff1a<\/p>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-399a346\"><code>theorem only_accept_if_signatory_and_time_elapsed :\n    \u2200 (datum: VestingDatum) (redeemer: VestingRedeemer) (scriptContext : ScriptContext) (time: POSIXTime),\n    \n    (isValidCtx scriptContext time) \u2192  \n    (validator datum redeemer scriptContext) \u2192\n\n    (scriptContext.transaction.signatories.contains datum.beneficiary\n     &amp;&amp;\n     time.time \u2265 datum.lock_until.time)<\/code><\/pre>\n\n\n\n<p class=\"deb-block deb-block-ff6e931\">\u3053\u306e\u5b9a\u7406\u304c\u610f\u5473\u3059\u308b\u306e\u306f\u4ee5\u4e0b\u306e\u901a\u308a\u3067\u3059\uff1a<\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-99a8b82\">\n<li class=\"\">datum\uff08\u30c7\u30fc\u30bf\uff09\u3001redeemer\uff08\u30ea\u30c7\u30a3\u30fc\u30de\u30fc\uff09\u3001scriptContext\uff08\u30b9\u30af\u30ea\u30d7\u30c8\u30b3\u30f3\u30c6\u30ad\u30b9\u30c8\uff09\u304c\u3069\u306e\u3088\u3046\u306a\u3082\u306e\u3067\u3042\u3063\u3066\u3082\u3001<\/li>\n\n\n\n<li class=\"\">time\uff08\u73fe\u5728\u6642\u523b\uff09\u304c\u305d\u306e\u6709\u52b9\u7bc4\u56f2\u5185\u306b\u3042\u308a\u3001<\/li>\n\n\n\n<li class=\"\">\u30d0\u30ea\u30c7\u30fc\u30bf\u304c true \u3092\u8fd4\u3057\u305f\u5834\u5408\u306b\u306f\u3001<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-a9d5d55\">\u4ee5\u4e0b\u306e\u6761\u4ef6\u304c\u5fc5\u305a\u6210\u7acb\u3057\u3066\u3044\u306a\u3051\u308c\u3070\u306a\u3089\u306a\u3044\uff1a<\/p>\n\n\n\n<ol start=\"1\" class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-2ad3274\">\n<li class=\"\">\u30c8\u30e9\u30f3\u30b6\u30af\u30b7\u30e7\u30f3\u306e\u7f72\u540d\u8005\u30ea\u30b9\u30c8\u306b\u3001\u30c7\u30fc\u30bf\u5185\u3067\u6307\u5b9a\u3055\u308c\u305f\u53d7\u76ca\u8005\u304c\u542b\u307e\u308c\u3066\u3044\u308b<\/li>\n\n\n\n<li class=\"\">\u73fe\u5728\u306e\u6642\u523b\u304c\u3001\u30c7\u30fc\u30bf\u5185\u3067\u6307\u5b9a\u3055\u308c\u305f\u30ed\u30c3\u30af\u89e3\u9664\u6642\u9593\uff08lock_until\uff09\u3088\u308a\u3082\u5927\u304d\u3044<\/li>\n<\/ol>\n\n\n\n<p class=\"deb-block deb-block-e32f7e1\">\u79c1\u305f\u3061\u306e\u30c4\u30fc\u30eb\u306f\u3053\u306e\u5b9a\u7406\u3092\u81ea\u52d5\u7684\u306bSMT\u30af\u30a8\u30ea\u306b\u5909\u63db\u3057\uff08\u3053\u308c\u306f\u958b\u767a\u8005\u304c\u76f4\u63a5\u8aad\u3080\u3082\u306e\u3067\u306f\u3042\u308a\u307e\u305b\u3093\uff09\u3001SMT\u30bd\u30eb\u30d0\u30fc\u306b\u9001\u4fe1\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-ff2a52a\" id=\"smte382bde383abe38390e383bce381aee7b590e69e9cefbc9ae5ae9ae79086e381afe581bdefbc81-18\"><strong>SMT\u30bd\u30eb\u30d0\u30fc\u306e\u7d50\u679c\uff1a\u5b9a\u7406\u306f\u507d\uff01<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-0fa3e14\">SMT\u30bd\u30eb\u30d0\u30fc\u306f\u3053\u306e\u5b9a\u7406\u304c\u507d\uff08Falsified\uff09\u3067\u3042\u308b\u3068\u5831\u544a\u3057\u307e\u3057\u305f\u3002\u30c4\u30fc\u30eb\u306f\u4ee5\u4e0b\u306e\u3088\u3046\u306a\u53cd\u4f8b\uff08\u30c6\u30b9\u30c8\u30b1\u30fc\u30b9\uff09\u3092\u51fa\u529b\u3057\u307e\u3057\u305f\uff08\u53ef\u8aad\u6027\u306e\u305f\u3081\u306b\u4e00\u90e8\u6574\u7406\u6e08\u307f\uff09\uff1a<\/p>\n\n\n\n<p class=\"deb-block deb-block-67bc1eb\">\u274c <strong>\u507d\uff08Falsified\uff09<\/strong><\/p>\n\n\n\n<p class=\"deb-block deb-block-367cd00\"><strong>\u53cd\u4f8b\uff1a<\/strong><\/p>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-1ec3fa7\">\n<li class=\"\">datum\uff1a<\/li>\n<\/ul>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-e73e1e9\"><code>{\n  lock_until: 1,\n  beneficiary: 0\n}<\/code><\/pre>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-1cca6a3\">\n<li class=\"\"><br><\/li>\n\n\n\n<li class=\"\">time\uff1a<\/li>\n<\/ul>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-77c8280\"><code>0<\/code><\/pre>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-22da4d2\">\n<li class=\"\"><br><\/li>\n\n\n\n<li class=\"\">scriptContext\uff1a<\/li>\n<\/ul>\n\n\n\n<pre class=\"wp-block-code deb-block deb-block-961ac72\"><code>{\n  purpose: Spending,\n  signatories: &#91;0],\n  validity_range: &#91;0, 11798],\n  ...\n}<\/code><\/pre>\n\n\n\n<ul class=\"wp-block-list wp-block-list list-col-1 inline-img-left deb-block deb-block-978bc39\">\n<li class=\"\"><br><\/li>\n\n\n\n<li class=\"\">redeemer: 8335<\/li>\n<\/ul>\n\n\n\n<p class=\"deb-block deb-block-76ba464\">\u3053\u306e\u53cd\u4f8b\u304b\u3089\u660e\u3089\u304b\u306b\u306a\u308b\u306e\u306f\u3001timeHasElapsed \u95a2\u6570\u306e\u691c\u67fb\u30ed\u30b8\u30c3\u30af\u306b\u8aa4\u308a\u304c\u3042\u308b\u3068\u3044\u3046\u3053\u3068\u3067\u3059\u3002\u5b9f\u969b\u3001validity_range \u306e\u4e0a\u9650\u304c\u5341\u5206\u9ad8\u3051\u308c\u3070\uff08\u3053\u306e\u4f8b\u3067\u306f11798\u3002\u30bd\u30eb\u30d0\u30fc\u304c\u3084\u3084\u904e\u5270\u306b\u8a2d\u5b9a\uff09\u3001\u5b9f\u969b\u306e\u6642\u9593\u304c\u307e\u3060\u7d4c\u904e\u3057\u3066\u3044\u306a\u304f\u3066\u3082\uff08\u73fe\u5728\u6642\u523b\u306f0\u3001\u30ed\u30c3\u30af\u306f1\u307e\u3067\uff09\u3001\u53d7\u76ca\u8005\u304c\u8cc7\u91d1\u3092\u5f15\u304d\u51fa\u305b\u3066\u3057\u307e\u3044\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-683f64a\">\u3053\u306e\u30b7\u30ca\u30ea\u30aa\u306f\u3001VacuumLabs\u306eCTF\u30c1\u30e3\u30ec\u30f3\u30b8\u306e\u4e2d\u3067\u3082\u3001\u4e0a\u9650\u3092\u975e\u5e38\u306b\u9ad8\u304f\u8a2d\u5b9a\u3059\u308b\u3053\u3068\u3067\u518d\u73fe\u30fb\u691c\u8a3c\u3067\u304d\u307e\u3059\u3002<\/p>\n\n\n\n<h4 class=\"wp-block-heading deb-block deb-block-d0ef282\" id=\"e4bb8ae5be8ce381aee5b195e69c9b-19\"><strong>\u4eca\u5f8c\u306e\u5c55\u671b<\/strong><\/h4>\n\n\n\n<p class=\"deb-block deb-block-cf9bee3\">\u3053\u308c\u306f\u3001\u4eca\u5f8c\u7d9a\u304f\u30b7\u30ea\u30fc\u30ba\u8a18\u4e8b\u306e\u7b2c\u4e00\u5f3e\u3067\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-4747c7a\">\u6b21\u56de\u306e\u8a18\u4e8b\u3067\u306f\u3055\u3089\u306b\u6df1\u304f\u6398\u308a\u4e0b\u3052\u3001UPLC\u30b3\u30fc\u30c9\uff08Cardano\u306e\u4f4e\u30ec\u30d9\u30eb\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u8a00\u8a9e\uff09\u3092\u3001Lean4\u3067\u518d\u5b9f\u88c5\u3057\u305fCEK\u30de\u30b7\u30f3\u304a\u3088\u3073Plutus Core\u306e\u4ed5\u7d44\u307f\u3092\u7528\u3044\u3066\u3001\u3069\u306e\u3088\u3046\u306b\u81ea\u52d5\u7684\u306b\u5f62\u5f0f\u7684\u8a3c\u660e\u3067\u304d\u308b\u304b\u3092\u7d39\u4ecb\u3057\u307e\u3059\u3002<\/p>\n\n\n\n<p class=\"deb-block deb-block-ea7bdaf\">\u3053\u306e\u4ed5\u7d44\u307f\u3092\u5b9f\u969b\u306e\u30d7\u30ed\u30c0\u30af\u30b7\u30e7\u30f3\u30b3\u30fc\u30c9\u4e0a\u3067\u5b9f\u6f14\u3057\u3001\u3055\u3089\u306b\u3053\u306e\u30c4\u30fc\u30eb\u304c\u3001\u30b3\u30fc\u30c9\u30ec\u30d9\u30eb\u3067\u65bd\u3055\u308c\u305f\u6700\u9069\u5316\u306e\u6b63\u5f0f\u306a\u8a3c\u660e\u306b\u3082\u6d3b\u7528\u3067\u304d\u308b\u3053\u3068\u3092\u793a\u3057\u3066\u3044\u304d\u307e\u3059\u3002<\/p>\n","protected":false},"excerpt":{"rendered":"\u30ab\u30eb\u30c0\u30ce\u306b\u8a2a\u308c\u308b\u65b0\u6642\u4ee3\uff1a\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u691c\u8a3c\u306e\u5b8c\u5168\u81ea\u52d5\u5316\u3078 Lean4\u3068Z3\u304c\u5207\u308a\u62d3\u304f\u3001\u958b\u767a\u8005\u30d5\u30ec\u30f3\u30c9\u30ea\u30fc\u306a\u30d5\u30a9\u30fc\u30de\u30eb\u30fb\u30d9\u30ea\u30d5\u30a3\u30b1\u30fc\u30b7\u30e7\u30f3 2025\u5e747\u670817\u65e5\u3001IOG\uff08Input Output Global\uff09\u306f\u3001\u30ab\u30eb\u30c0\u30ce\u306b\u304a\u3051\u308b\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u5b89\u5168\u6027\u3068\u4fe1\u983c\u6027\u3092\u98db\u8e8d\u7684\u306b\u9ad8\u3081\u308b\u65b0\u30c4\u30fc\u30eb\u306e\u958b\u767a\u3092\u516c\u8868\u3057\u307e\u3057\u305f\u3002\u3053\u306e\u30c4\u30fc\u30eb\u306f\u3001\u958b\u767a\u8005\u306e\u624b\u3092\u7169\u308f\u305b\u308b\u3053\u3068\u306a\u304f\u3001\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306e\u300c\u5f62\u5f0f\u7684\u691c\u8a3c\uff08formal verification\uff09\u300d\u3092\u5b8c\u5168\u81ea\u52d5\u3067\u5b9f\u884c\u3067\u304d\u308b\u753b\u671f\u7684\u306a\u3082\u306e\u3067\u3059\u3002 \u306a\u305c\u5f62\u5f0f\u7684\u691c\u8a3c\u304c\u5fc5\u8981\u306a\u306e\u304b\uff1f \u30ab\u30eb\u30c0\u30ce\u306e\u30b9\u30de\u30fc\u30c8\u30b3\u30f3\u30c8\u30e9\u30af\u30c8\u306f\u3001Plinth\u3001Aiken\u3001Plu-ts\u306a\u3069\u306e\u9ad8\u6c34\u6e96\u8a00\u8a9e\u3067\u8a18\u8ff0\u3055\u308c\u3001\u5b9f\u969b\u306e\u8cc7\u7523\u3092\u76f4\u63a5\u5236\u5fa1\u3057\u3066\u3044\u307e\u3059&hellip;","protected":false},"author":1,"featured_media":42330,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[67,21,35,1,38],"tags":[],"class_list":{"0":"post-42329","1":"post","2":"type-post","3":"status-publish","4":"format-standard","5":"has-post-thumbnail","7":"category-iog","8":"category-21","9":"category-blog","10":"category-japanese","11":"category-38"},"featured_image_urls":{"full":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp",800,450,false],"thumbnail":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-150x150.webp",150,150,true],"medium":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-300x169.webp",300,169,true],"medium_large":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-768x432.webp",768,432,true],"large":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp",800,450,false],"1536x1536":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp",800,450,false],"2048x2048":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp",800,450,false],"dp-widget-thumb":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-140x96.webp",140,96,true],"dp-widget-thumb-2x":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-280x192.webp",280,192,true],"dp-related-thumb":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-250x154.webp",250,154,true],"dp-related-thumb-2x":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-500x308.webp",500,308,true],"dp-archive-thumb":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1-450x253.webp",450,253,true],"dp-archive-thumb-2x":["https:\/\/sipo.tokyo\/wp-content\/uploads\/2025\/07\/\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9-1.webp",800,450,false]},"category_list":"<a href=\"https:\/\/sipo.tokyo\/?cat=67\" rel=\"category\">IOG\u30d6\u30ed\u30b0<\/a>, <a href=\"https:\/\/sipo.tokyo\/?cat=21\" rel=\"category\">\u30cb\u30e5\u30fc\u30b9<\/a>, <a href=\"https:\/\/sipo.tokyo\/?cat=35\" rel=\"category\">\u30d6\u30ed\u30b0<\/a>, <a href=\"https:\/\/sipo.tokyo\/?cat=1\" rel=\"category\">\u65e5\u672c\u8a9e\u7248<\/a>, <a href=\"https:\/\/sipo.tokyo\/?cat=38\" rel=\"category\">\u7ffb\u8a33<\/a>","author_info":{"name":"sition","url":"https:\/\/sipo.tokyo\/?author=1"},"comments_num":"0 comments","_links":{"self":[{"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/posts\/42329","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=42329"}],"version-history":[{"count":5,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/posts\/42329\/revisions"}],"predecessor-version":[{"id":42335,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/posts\/42329\/revisions\/42335"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=\/wp\/v2\/media\/42330"}],"wp:attachment":[{"href":"https:\/\/sipo.tokyo\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=42329"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=42329"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sipo.tokyo\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=42329"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}