The reflective Milawa theorem prover is sound (down to the machine code that runs it). (English) Zbl 1356.68186

Summary: This paper presents, we believe, the most comprehensive evidence of a theorem prover’s soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an idealised version of ACL2’s computational logic and provides the user with high-level tactics similar to ACL2’s. In contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat like an LCF-style system. We explain how the Milawa theorem prover is constructed as a sequence of reflective extensions from its kernel. The kernel establishes the soundness of these extensions during Milawa’s bootstrapping process. Going deeper, we explain how we have shown that the Milawa kernel is sound using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved the logic sound, and proved that the source code for the Milawa kernel (1,700 lines of Lisp) faithfully implements this logic. Going even further, we have combined these results with the x86 machine-code level verification of the Lisp runtime Jitawa. Our top-level theorem states that Milawa can never claim to prove anything that is false when it is run on this Lisp runtime.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 576-580, (1969) · Zbl 0179.23105
[2] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)
[3] Bertot, Y; Castéran, P, Interactive theorem proving and program development: coq’art: the calculus of inductive constructions, (2004), Berlin · Zbl 1069.68095
[4] Slind, K; Norrish, M; Mohamed, OA (ed.); Muñoz, C (ed.); Tahar, S (ed.), A brief overview of HOL4, (2008), Berlin · Zbl 1165.68474
[5] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic Volume 2283 of LNCS. Springer, Berlin Heidelberg (2002) · Zbl 0994.68131
[6] Davis, J.C.: A Self-Verifying Theorem Prover. PhD thesis, University of Texas, Austin (2009)
[7] Boyer, RS; Kaufmann, M; Moore, JS, The boyer-Moore theorem prover and its interactive enhancement, Comput. Math. Appl., 29, 27-62, (1995)
[8] Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, Springer, Berlin (1979) · Zbl 0421.68039
[9] Harrison, J; Berghofer, S (ed.); Nipkow, T (ed.); Urban, C (ed.); Wenzel, M (ed.), HOL light: an overview, (2009), Berlin · Zbl 1252.68255
[10] Myreen, MO; Davis, J, A verified runtime for a verified theorem prover, (2011), Berlin · Zbl 1342.68297
[11] Harrison, J; Furbach, U (ed.); Shankar, N (ed.), Towards self-verification of HOL light, (2006), Berlin · Zbl 1222.68364
[12] Griffioen, D; Huisman, M; Gundy, J (ed.); Newey, M (ed.), A comparison of PVS and isabelle/HOL, 123-142, (1998), Berlin
[13] Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: SMT ’09, ACM, pp. 1-5 (2009)
[14] Brummayer, R; Lonsing, F; Biere, A, Automated testing and debugging of SAT and QBF solvers, 44-57, (2010), Berlin · Zbl 1306.68155
[15] Järvisalo, M; Heule, MJ; Biere, A; Gramlich, B (ed.); Miller, D (ed.); Sattler, U (ed.), Inprocessing rules, 355-370, (2012), Berlin · Zbl 1358.68256
[16] Barendregt, H; Wiedijk, F, The challenge of computer mathematics, Phil. Trans. R. Soc. A, 363, 2351-2375, (2005) · Zbl 1152.03304
[17] Wetzler, N; Heule, M; Hunt, WAJr, DRAT-trim: efficient checking and trimming using expressive clausal proofs, 422-429, (2014), Berlin · Zbl 1423.68475
[18] Balabanov, V; Jiang, JR, Unified qbf certification and its applications, Form. Methods Syst. Des., 41, 45-65, (2012) · Zbl 1284.68516
[19] Böhme, S; Fox, A; Sewell, T; Weber, T, Reconstruction of Z3’s bit-vector proofs in HOL4 and isabelle/HOL, 183-198, (2011), Berlin · Zbl 1350.68225
[20] McCune, W; Shumsky, O, Ivy: a preprocessor and proof checker for first-order logic, (2000), Norwell
[21] Darbari, A; Fischer, B; Marques-Silva, J, Industrial-strength certified SAT solving through verified SAT proof checking, 260-274, (2010), Berlin
[22] Weber, T; Amjad, H, Efficiently checking propositional refutations in HOL theorem provers, J. Appl. Logic, 7, 26-40, (2009) · Zbl 1171.68041
[23] Marić, F, Formalization and implementation of modern SAT solvers, J. Autom. Reason., 43, 81-119, (2009) · Zbl 1187.68557
[24] Hurd, J; Bobaru, M (ed.); Havelund, K (ed.); Holzmann, GJ (ed.); Joshi, R (ed.), The opentheory standard theory library, (2011), Berlin
[25] Kaufmann, M; Moore, JS, Structured theory development for a mechanized logic, J. Autom. Reason., 26, 161-203, (2001) · Zbl 0971.03017
[26] Davis, J.: Reasoning about file input in ACL2. In: Manolios, P., Wilding, M. (eds.) ACL2 ’06 (2006)
[27] Kaufmann, M., Moore, J.: Design goals of ACL2. Technical Report 101, Computational Logic, Inc. (1994)
[28] Rager, D.L., Hunt, W.A. Jr.: Implementing a parallelism library for a functional subset of LISP. In: International Lisp Conference (ILC), pp. 18-30 (2009) · Zbl 1284.68516
[29] Boyer, R.S., Hunt, W.A. Jr.: Function memoization and unique object representation for ACL2 functions. In: ACL2 ’06, ACM (2006) · Zbl 1342.68297
[30] Hunt, WAJr; Krug, RB; Moore, J; Geist, D (ed.), Linear and nonlinear arithmetic in ACL2, 319-333, (2003), Berlin · Zbl 1179.68136
[31] Hunt, WAJr; Kaufmann, M; Krug, RB; Moore, J; Smith, EW; Hurd, J (ed.); Melham, T (ed.), Meta reasoning in ACL2, 163-178, (2005), Berlin · Zbl 1152.68522
[32] Brock, B; Kaufmann, M; Moore, JS, Rewriting with equivalence relations in ACL2, J. Autom. Reason., 40, 293-306, (2008) · Zbl 1140.68029
[33] Kaufmann, M; Moore, JS; Ray, S; Reeber, E, Integrating external deduction tools with acl2, J. Autom. Reason., 7, 3-25, (2009) · Zbl 1183.68558
[34] Harrison, J.: Metatheory and reflection in theorem proving: a survey and critique. Technical Report CRC-053. SRI Cambridge, Millers Yard, Cambridge, UK (1995) · Zbl 1208.68205
[35] McCarthy, J, Recursive functions of symbolic expressions and their computation by machine, part 1, Commun. ACM, 3, 184-195, (1960) · Zbl 0101.10413
[36] Shoenfield, J.R.: Mathematical Logic. The Association for Symbolic Logic (1967) · Zbl 0155.01102
[37] Shankar, N.: Metamathematics, Machines, and Gödel’s Proof. Cambridge University Press, Cambridge (1994) · Zbl 0813.68150
[38] Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, New York (1997) · Zbl 0655.68117
[39] Myreen, MO; Gordon, MJC; Berghofer, S (ed.); Nipkow, T (ed.); Urban, C (ed.); Wenzel, M (ed.), Verified LISP implementations on ARM, x86 and powerpc, (2009), Berlin
[40] Kaufmann, M; Slind, K; Schneider, K (ed.); Brandt, J (ed.), Proof pearl: wellfounded induction on the ordinals up to 𝜖0, 294-301, (2007), Berlin · Zbl 1144.68361
[41] Myreen, MO, Functional programs: conversions between deep and shallow embeddings, (2012), Berlin
[42] Myreen, M.O.: Verified just-in-time compiler on x86. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL), ACM (2010) · Zbl 1312.68046
[43] Myreen, M.O.: Formal verification of machine-code programs. PhD thesis, University of Cambridge, Cambridge (2009)
[44] Myreen, MO; Slind, K; Gordon, MJ; de Moor, O (ed.); Schwartzbach, MI (ed.), Extensible proof-producing compilation, (2009), Berlin
[45] Manolios, P; Moore, JS, Partial functions in ACL2, J. Autom. Reason., 31, 107-127, (2003) · Zbl 1060.68109
[46] Kumar, R; Arthan, R; Myreen, MO; Owens, S; Klein, G (ed.); Gamboa, R (ed.), HOL with definitions: semantics, soundness, and a verified implementation, (2014), Berlin · Zbl 1416.68167
[47] Myreen, MO; Owens, S; Kumar, R; Blazy, S (ed.); Paulin-Mohring, C (ed.); Pichardie, D (ed.), Steps towards verified implementations of HOL light, (2013), Berlin · Zbl 1317.68225
[48] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL), ACM (2014) · Zbl 1284.68405
[49] Gordon, M.J.C., Hunt, W.A. Jr., Kaufmann, M., Reynolds, J.: An embedding of the ACL2 logic in HOL. In: International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2), ACM, pp. 40-46 (2006)
[50] Gordon, M.J.C., Reynolds, J., Hunt, W.A. Jr., Kaufmann, M.: An integration of HOL and ACL2. In: Formal Methods in Computer-Aided Design (FMCAD). IEEE Computer Society, pp. 153-160 (2006)
[51] McCune, W; Shumsky, O, System description: ivy, 401-405, (2000), Berlin · Zbl 0963.68527
[52] Ridge, T; Margetson, J; Hurd, J (ed.); Melham, TF (ed.), A mechanically verified, sound and complete theorem prover for first order logic, (2005), Berlin · Zbl 1152.03316
[53] Marić, F, Formal verification of a modern SAT solver by shallow embedding into isabelle/HOL, Theor. Comput. Sci., 411, 4333-4356, (2010) · Zbl 1208.68205
[54] Haftmann, F., Bulwahn, L.: Code generation from Isabelle/HOL theories Isabelle2011-1 Documentation. http://isabelle.in.tum.de · Zbl 1060.68109
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.