Finite Field
ตรวจเบื้องต้น 30 วินาที

MPK Assurance / ตรวจความพร้อมในการพิสูจน์โค้ด Go

เราพิสูจน์
โค้ด Go ของคุณ ไม่ใช่แค่ทดสอบ

เราตรวจสอบตรรกะ Go สำคัญที่เกี่ยวข้องกับเงิน เช่น การคืนเงิน ค่าธรรมเนียม ยอดคงเหลือ และเงินสำรอง เทียบกับข้อกำหนด สมมติฐาน และขอบเขตที่ระบุอย่างชัดเจน Gemini เตรียมร่างหลักฐาน และเคอร์เนล MPK อิสระเป็นผู้ตัดสินขั้นสุดท้าย

ลองเดโมคืนเงิน 30 วินาที ขอตรวจความพร้อมในการพิสูจน์
จำกัดเฉพาะ 5 บริษัทแรก ข้อเสนอสำหรับผู้เริ่มใช้ MPK ระยะแรก JPY 49,800(ยังไม่รวมภาษี)
เริ่มจากฟังก์ชัน Go หนึ่งตัว
ตรวจได้สูงสุด 2 คุณสมบัติ
ไม่ต้องกรอก
โค้ดลับในที่สาธารณะ
ส่งมอบหลักฐาน
ที่ตรวจซ้ำได้

ตัวแก้ปัญหา MPK

สด
refund.go
func ApplyRefund(paid, refunded, amount int64) (int64, error) {
  if amount < 0 {
    return refunded, errors.New("negative amount")
  }
  if refunded+amount > paid {
    return refunded, errors.New("exceeds paid")
  }
  return refunded + amount, nil
}
คุณสมบัติที่ต้องตรวจสอบ

∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid

พบกรณีโต้แย้ง

paid=100, refunded=80, amount=30 ละเมิดคุณสมบัติที่กำหนด

เคอร์เนลตรวจสอบแล้ว

เคอร์เนลยอมรับใบรับรองมาตรฐานของเวอร์ชันที่แก้ไขแล้ว

การรับรองที่เหนือกว่าการทดสอบเริ่มจาก Go ปกติแยก AI ออกจากการตัดสินความน่าเชื่อถือแสดงหลักฐาน กรณีโต้แย้ง และส่วนที่ยกเว้น

เดโมคืนเงิน 30 วินาที

ค้นหากรณีโต้แย้ง แล้วพิสูจน์เวอร์ชันที่แก้ไขแล้ว

ลองโค้ดคืนเงินที่เตรียมไว้ แล้วดูขั้นตอนตั้งแต่พบกรณีโต้แย้ง แก้ไข ไปจนถึงพิสูจน์สำเร็จ คุณไม่ต้องกรอกโค้ดลับในเดโมสาธารณะ

นโยบายการคืนเงิน: ยอดคืนเงินสะสมต้องไม่เกินยอดที่ชำระแล้ว

คุณสมบัติที่ต้องตรวจสอบ

0 ≤ refunded + amount ≤ paid
  • เป้าหมาย: ฟังก์ชันนโยบายคืนเงินหนึ่งตัว
  • ข้อมูลนำเข้า: จำนวนเต็มไม่ติดลบ
  • I/O ภายนอก ฐานข้อมูล และเครือข่ายอยู่นอกขอบเขต
  • ตรวจภายใต้สมมติฐานที่ระบุและชุดย่อยของ Go

ผลการตรวจสอบ (เวอร์ชันที่มีข้อบกพร่อง)

พบกรณีโต้แย้ง

เราพบข้อมูลนำเข้าที่ทำให้ยอดคืนเงินสะสมเกินยอดที่ชำระแล้ว

paid = 100
refunded = 80
amount = 30
ผลลัพธ์ = 110 (ละเมิดคุณสมบัติ)

รายละเอียดทางเทคนิค

รหัสการรัน
run_refund_bug_20260727
แฮชใบรับรอง
— ไม่ได้สร้างเพราะพบกรณีโต้แย้ง
คำตัดสินของเคอร์เนล
ปฏิเสธ / พบกรณีโต้แย้ง
รายงานสัจพจน์
เลขคณิตจำนวนเต็ม / สมมติฐานที่ระบุชัดเจน

การจำแนกผลลัพธ์

ผลลัพธ์ 4 ประเภท

พิสูจน์แล้ว

คุณสมบัติที่ระบุเป็นจริงภายใต้สมมติฐานและขอบเขตที่กำหนดชัดเจน

พิสูจน์แล้ว
พบกรณีโต้แย้ง

เราแสดงข้อมูลนำเข้าที่ละเมิดคุณสมบัติ และชี้ชัดว่าเงื่อนไขใดต้องแก้ไข

พบว่าขัดแย้ง
ยังสรุปไม่ได้

เรารายงานอย่างชัดเจนเมื่อกลยุทธ์ปัจจุบันยังตัดสินไม่ได้ว่าคุณสมบัตินั้นเป็นจริงหรือไม่

ยังสรุปไม่ได้
นอกขอบเขต

เราอธิบายเหตุผลเฉพาะที่ยังจัดการเป้าหมายไม่ได้ เช่น รูปแบบไวยากรณ์ที่ไม่รองรับ I/O ภายนอก หรือพฤติกรรมที่ไม่รองรับ

ใช้ไม่ได้กับขอบเขตนี้

ความต่างจากการทดสอบ

เราตรวจคุณสมบัติที่ระบุ ไม่ใช่แค่ข้อมูลนำเข้าที่เลือกไว้

การทดสอบแบบใช้ตัวอย่าง

  • รันเฉพาะกรณีที่เขียนไว้
  • ข้อมูลนำเข้าที่ไม่ได้เลือกยังไม่ถูกครอบคลุม
  • ผลผ่านการทดสอบไม่ใช่ใบรับรอง
  • ความน่าเชื่อถือขึ้นกับการออกแบบชุดทดสอบ

MPK Assurance (การพิสูจน์)

  • ตรวจคุณสมบัติและขอบเขตที่ระบุ
  • แสดงข้อมูลนำเข้าที่ทำให้คุณสมบัติถูกละเมิด
  • เหลือใบรับรองและแฮชที่ตรวจซ้ำได้
  • เคอร์เนลอิสระเป็นผู้ตัดสินขั้นสุดท้าย
รายการเปรียบเทียบการทดสอบการพิสูจน์
เป้าหมายข้อมูลนำเข้าที่เลือกคุณสมบัติที่ระบุ
การแสดงกรณีโต้แย้ง△○
ตรวจซ้ำบันทึกการรันใบรับรอง
การตัดสินขั้นสุดท้ายชุดทดสอบเคอร์เนล

คุณสมบัติหลัก 3 ข้อ

การรับรองที่เหนือกว่าการทดสอบ

เราตรวจคุณสมบัติเทียบกับข้อกำหนด สมมติฐาน และขอบเขตที่ระบุชัดเจน ไม่ใช่แค่ตัวอย่างไม่กี่ชุด

ใช้ Go ไม่ต้องใช้ภาษาพิสูจน์เฉพาะทาง

คุณเริ่มได้จากฟังก์ชันนโยบาย Go สำคัญที่แยกออกจาก I/O ภายนอกแล้ว

ให้ AI ช่วยพิสูจน์ แต่ไม่ให้ AI เป็นแหล่งความเชื่อถือ

AI ทำหน้าที่เตรียมร่างหลักฐานเท่านั้น การยอมรับขั้นสุดท้ายทำโดยเคอร์เนลอิสระที่อ่านใบรับรองมาตรฐาน

ให้ AI ทำงาน แต่ไม่ให้ AI ตัดสินขั้นสุดท้าย

ลูกค้าส่งฟังก์ชัน Go และคุณสมบัติที่ต้องการรับประกัน
Geminiเสนอคุณสมบัติ กลยุทธ์ และร่างหลักฐาน
MPKขอบเขตความเชื่อถือที่ตรวจใบรับรองอย่างอิสระ
ผู้รับผิดชอบยืนยันข้อกำหนด สมมติฐาน และการรักษาความลับ
หลักฐานส่งมอบชุดหลักฐานที่ตรวจซ้ำได้

Gemini ดำเนินเวิร์กโฟลว์พิสูจน์ MPK ตัดสินด้านความเชื่อถือ และผู้รับผิดชอบอนุมัติการส่งมอบ

กรณีที่การตรวจสอบช่วยได้มาก

การคืนเงินยอดคืนเงินสะสมต้องไม่เกินยอดที่ชำระแล้ว
ค่าธรรมเนียมต้องไม่ติดลบและต้องไม่เกินเพดานตามสัญญา
เงินสำรองยอดคงเหลือหลังประมวลผลต้องไม่ต่ำกว่าขั้นต่ำ
ส่วนลดยังอยู่ในขีดจำกัดแม้ใช้ส่วนลดซ้อนกัน
คะแนนคะแนนที่ออกให้ต้องไม่เกินวงเงินงบประมาณ
การจัดสรรยอดที่จัดสรรรวมกันต้องเท่ากับเงินต้นเดิม

ชุดหลักฐาน

เราส่งมอบหลักฐานที่ตรวจซ้ำได้ ไม่ใช่คำตอบจาก AI

ใบรับรอง MPK

การตรวจความพร้อมในการพิสูจน์
บันทึกใบรับรองมาตรฐาน

คำตัดสินของเคอร์เนล
ยอมรับแล้ว
MPK
  • แฮชใบรับรอง
  • คำตัดสินของเคอร์เนล MPK
  • ผลจากตัวตรวจอ้างอิงของ Go
  • รายงานสัจพจน์
  • คุณสมบัติที่พิสูจน์แล้วและสมมติฐานที่ระบุ
  • ขอบเขตที่ยกเว้นและเหตุผลที่อยู่นอกขอบเขต
  • กรณีโต้แย้ง หากพบ
  • รหัสการรันและข้อมูลสำหรับตรวจซ้ำ

การตรวจความพร้อมในการพิสูจน์

ตรวจฟังก์ชันแรกของคุณภายในขอบเขตที่กำหนดตายตัว

JPY 198,000 (ยังไม่รวมภาษี)
  • ฟังก์ชัน Go หนึ่งตัว
  • พิสูจน์ได้สูงสุด 2 คุณสมบัติ
  • จำแนกผลเป็นพิสูจน์แล้ว พบกรณีโต้แย้ง ยังสรุปไม่ได้ หรืออยู่นอกขอบเขต
  • ชุดหลักฐานและการอธิบายผลทางออนไลน์
ดูข้อเสนอสำหรับผู้เริ่มใช้ระยะแรก

นี่คือราคาปกติที่วางแผนไว้ ขณะนี้เรามีแคมเปญสำหรับผู้เริ่มใช้ระยะแรก จำกัดเฉพาะ 5 บริษัทแรก ในราคา JPY 49,800 ยังไม่รวมภาษี

ข้อเสนอสำหรับผู้เริ่มใช้ MPK ระยะแรก

จำกัดเฉพาะ 5 บริษัทแรก

ตรวจว่าโค้ด Go สำคัญของคุณสามารถพิสูจน์ได้ ไม่ใช่แค่ทดสอบหรือไม่

ในการตรวจความพร้อมในการพิสูจน์ของ MPK เราเลือกฟังก์ชัน Go เป้าหมายหนึ่งตัว กำหนดคุณสมบัติที่ต้องรับประกัน สร้างร่างหลักฐานด้วย AI และให้เคอร์เนล MPK ตรวจสอบอย่างอิสระ

สิ่งที่รวมอยู่

  • ฟังก์ชัน Go หนึ่งตัว
  • พิสูจน์ได้สูงสุด 2 คุณสมบัติ
  • การประเมินความเข้ากันได้กับ MPK
  • รายงานเกี่ยวกับหลักฐาน กรณีโต้แย้ง สิ่งที่ขวางการพิสูจน์ และรายการนอกขอบเขต
  • รายงานสรุปขอบเขตการพิสูจน์และสมมติฐาน

เงื่อนไขแคมเปญ

ข้อเสนอนี้สำหรับบริษัทที่สามารถให้ความคิดเห็นอย่างตรงไปตรงมาหลังจบบริการ และอนุมัติกรณีศึกษาเพื่อเผยแพร่บนเว็บไซต์ทางการของ MPK กรณีศึกษาอาจมีชื่อบริษัท ชื่อผู้ติดต่อ ตำแหน่ง ความคิดเห็น และรูปตัวแทนหรือโลโก้บริษัท

ชื่อบริษัทชื่อตำแหน่งความคิดเห็นรูปตัวแทนหรือโลโก้บริษัท
คุณจะได้ตรวจเนื้อหาก่อนเผยแพร่ และเราจะใช้เฉพาะวัสดุที่ได้รับอนุมัติเท่านั้น เราไม่ขอรีวิวเชิงบวก

ขั้นตอนบริการ

ขั้นตอนบริการ (5 ขั้นตอน)

ค้นหาประเด็น

ยืนยันสถานการณ์ข้อผิดพลาดที่อาจก่อความเสียหายและฟังก์ชันเป้าหมาย

กำหนดขอบเขตตายตัว

ตรึงฟังก์ชัน คุณสมบัติ สมมติฐาน และขอบเขตที่ยกเว้น

การตรวจทานด้วย Gemini + MPK

AI เตรียมร่างหลักฐาน และ MPK ตรวจใบรับรอง

อธิบายผลลัพธ์

อธิบายหลักฐาน กรณีโต้แย้ง ผลที่ยังสรุปไม่ได้ ส่วนที่ยกเว้น และหลักฐานประกอบ

ขั้นตอนถัดไป

ชี้ชัดว่าจะเดินหน้าสู่การแก้ไข ฟังก์ชันเพิ่มเติม หรือการเชื่อมต่อ CI/CD หรือไม่

เหมาะที่สุดกับ

  • คุณพัฒนาตรรกะคืนเงิน ค่าธรรมเนียม หรือยอดคงเหลือด้วย Go
  • ข้อบกพร่องเพียงจุดเดียวอาจทำให้เกิดความเสียหายทางการเงินหรือภาระงานตรวจสอบ
  • คุณยังไม่มีทีมพิสูจน์เชิงรูปนัยโดยเฉพาะ
  • คุณมีฟังก์ชันขนาดเล็กที่แยกออกจาก I/O ภายนอกได้

ข้อจำกัดปัจจุบัน

  • การพิสูจน์แอปพลิเคชัน Go ทั้งหมดแบบไม่จำกัดขอบเขต
  • กระบวนการตั้งแต่ต้นจนจบที่รวม DB, API, เครือข่าย หรือ UI
  • การตรวจจับช่องโหว่ความปลอดภัยทุกประเภท
  • รูปแบบไวยากรณ์ที่ไม่รองรับ ไลบรารีพึ่งพาภายนอก หรือข้อกำหนดที่ไม่ชัดเจน

คำถามที่พบบ่อย

คำถามที่พบบ่อยก่อนการปรึกษาครั้งแรก

คำตอบเหล่านี้ครอบคลุมคำถามที่พบบ่อยก่อนติดต่อเรา เช่น ขอบเขตการพิสูจน์ บทบาทของ AI และวิธีจัดการโค้ด

สิ่งนี้กำจัดบั๊กทั้งหมดหรือไม่?

ไม่ เราตรวจเฉพาะคุณสมบัติที่ระบุ ภายใต้สมมติฐาน ขอบเขต และชุดย่อยของ Go ที่รองรับเท่านั้น จึงไม่รับประกันทั้งแอปพลิเคชันหรือระบบภายนอกทั้งหมด

ต้องเรียน Lean หรือ Rocq หรือไม่?

ไม่จำเป็นสำหรับการตรวจครั้งแรก เราเริ่มจากการยืนยันฟังก์ชันนโยบาย Go ที่แยกจาก I/O ภายนอก และคุณสมบัติที่ต้องการรับประกัน

AI เป็นผู้ตัดสินว่าอะไรถูกต้องหรือไม่?

ไม่ Gemini สร้างคุณสมบัติ กลยุทธ์การพิสูจน์ และร่างหลักฐาน ส่วนเคอร์เนล MPK อิสระเป็นผู้ยอมรับหรือปฏิเสธใบรับรองขั้นสุดท้าย

ถ้าพิสูจน์ไม่ผ่านจะเกิดอะไรขึ้น?

เราจำแนกผลเป็นพบกรณีโต้แย้ง ยังสรุปไม่ได้ หรืออยู่นอกขอบเขต จากนั้นอธิบายเหตุผล ข้อกำหนดที่จำเป็น แนวทางแก้ไขที่เป็นไปได้ และวิธีแยกหน่วยที่พิสูจน์ได้

เชื่อมต่อกับ CI/CD ได้หรือไม่?

หลังจากการตรวจความพร้อมในการพิสูจน์ยืนยันเป้าหมายและความเป็นไปได้แล้ว เราสามารถเสนอการตรวจต่อเนื่องหรือการเชื่อมต่อ CI/CD แยกต่างหากได้

ต้องส่งโค้ดมากับคำถามหรือไม่?

คุณไม่ต้องวางโค้ดลับในฟอร์มสาธารณะ หลังจากติดต่อมา เราจะยืนยันการจัดการ NDA และวิธีแชร์ที่ปลอดภัย

ติดต่อ

ตรวจว่าโค้ดของคุณพิสูจน์ได้หรือไม่

บอกเราว่าข้อผิดพลาดแบบใดสำคัญที่สุด และต้องการให้ตรวจฟังก์ชัน Go ใด คุณไม่ต้องวางโค้ดลับในฟอร์มสาธารณะ

รองรับ NDA และการแชร์โค้ดอย่างปลอดภัย

อย่ากรอกซอร์สโค้ด ข้อมูลรับรอง หรือข้อมูลส่วนบุคคลในฟอร์มสาธารณะ

ได้รับข้อมูลตัวอย่างแล้ว ในเว็บไซต์จริงให้เชื่อมต่อกับขั้นตอนรับคำถามที่มีอยู่