Applying Formal Methods to the Events of the Resurrection
In honor of Resurrection Day this year, let’s take a moment to apply formal methods in reverse, as though we were detectives, in order to back out the timeline of the week when Christ was crucified.
Specifically, I’d like to investigate the timing of a couple of events that took place leading up to Resurrection day. These events include:
- The last supper,
- The night of prayer in Gethsemane,
- The crucifixion,
- The time He spent in the tomb, and
- The visit to the tomb early on Sunday morning
We can express these events as inputs to a design, so we’ll constrain them using assumptions:
You may notice that I’ve added a couple other items into the timeline as well, such as when the chief priests requested guards for the temple and when the women prepared the spices they then later brought to the tomb. We’ll discuss these more as we go along. I’ve also added in inputs for the preparation days and the Sabbath(s), because those will become important in this discussion as well.
Our goal will be to let the formal tool, in this case SymbiYosys as a front-end for the yices engine, solve for the timing of these events, subject to the formal constraints we’ll discuss below.
Creating a framework for our events
Part of the goal here is to determine when events took place. This means that we need a structure we can use to describe the events of interest.
We’ll also use synchronous logic, and so that means that we’ll start with the
i_clk. Let’s assume that it has a period of twice
per day, with the rising edge at both dawn and dusk. While I understand
that this will cause the duty cycle to vary somewhat, I’m not really
expecting any struggles to meet timing if we run the clock this slowly.
This clock speed will also allow us to reason about whether an event happened
during the day or during the night. To get there, we’ll use a counter to
describe time for us–to include which day of the week, Sunday, Monday,
Tuesday, etc., an event is taking place on. We can do all of this with
a 14-state counter, such as the counter below that goes from
0 on Sunday
13 on Saturday and back again.
Further, in Jewish fashion dating back to the beginning,
And God called the light Day, and the darkness he called Night. And the evening and the morning were the first day. (Gen 1:5)
we’ll count days that begin and end at sundown.
We’ll also assign days to counter values, so we can later make sense of the trace SymbiYosys will generate for us.
Fig. 1 below should give you an idea of what this might look like.
Now we can now couple this counter with inferences from the Bible. For example, we know that the Sabbath takes place on Saturday.
We also know that the Sabbath begins or ends at nighttime.
Let’s see where this all leads us.
It all starts with the last supper
While I suppose we might start with the triumphal entry, I’d rather start our reasoning off with the Last Supper:
Now before the feast of the passover, when Jesus knew that his hour was come that he should depart out of this world unto the Father, having loved his own which were in the world, he loved them unto the end. And supper being ended, the devil having now put into the heart of Judas Iscariot, Simon’s son, to betray him; (John 13:1-2)
For those not familiar with the Last Supper, this was the night when,
… he took bread, and gave thanks, and brake it, and gave unto them, saying, This is my body which is given for you: this do in remembrance of me. Likewise also the cup after supper, saying, This cup is the new testament in my blood, which is shed for you. (Luke 22:19-20)
But that’s not my point today. Today, I just want to work through the order of events.
The Last Supper is then followed by an evening in the Garden of Gethsemane.
When Jesus had spoken these words, he went forth with his disciples over the brook Cedron, where was a garden, into the which he entered, and his disciples. (John 18:1)
From this, we know that the last supper occurred in the day time,
and that it was followed by the night in Gethsemane.
This isn’t quite enough of a constraint to force the night in Gethsemane to
immediately (and only ever) follow
i_last_supper. We also need to tell the
formal tool that the night in Gethsemane only occurs following the
last supper, and never at any other time.
The night in the Garden
After the Last Supper, Jesus went to pray in the Garden of Gethsemane.
Then cometh Jesus with them unto a place called Gethsemane, and saith unto the disciples, Sit ye here, while I go and pray yonder. (Matt 26:36)
It was here, in the garden, that Luke, the beloved physician, records that his prayers were so agonizing that He sweat blood.
And being in an agony he prayed more earnestly: and his sweat was as it were great drops of blood falling down to the ground. (Luke 22:44)
We know this took place at night because, among other things, his disciples were struggling to stay awake.
And he came and found them asleep again: for their eyes were heavy. And he left them, and went away again, and prayed the third time, saying the same words. (Matt 26:43-44)
Hence, we can assume that the night in Gethsemane,
took place during
You may perhaps be wondering why I have chosen this backwards notation.
Could I not have instead said that,
i_gethsemane |-> nighttime?
Probably. However, I’m trying to capture the idea that the signal
I am assuming should be on the right hand of the implication. Therefore, the
backwards notation is primarily to make plain which value I’m intending to
constrain with the assumption.
Returning to the timeline, it was in Gethsemane that Jesus was betrayed and arrested.
Then cometh he to his disciples, and saith unto them, Sleep on now, and take your rest: behold, the hour is at hand, and the Son of man is betrayed into the hands of sinners. Rise, let us be going: behold, he is at hand that doth betray me.
And while he yet spake, lo, Judas, one of the twelve, came, and with him a great multitude with swords and staves, from the chief priests and elders of the people. (Matt 26:45-47)
On the next day, after a sham trial, the chief priests and elders led Jesus to Pilate.
When the morning was come, all the chief priests and elders of the people took counsel against Jesus to put him to death: And when they had bound him, they led him away, and delivered him to Pontius Pilate the governor. (Matt 27:1-2)
While I’m sure they would’ve loved to murder Him themselves, the Romans had a law prohibiting the Jews from executing those they chose.
Then said Pilate unto them, Take ye him, and judge him according to your law. The Jews therefore said unto him, It is not lawful for us to put any man to death: (John 18:31)
Therefore, we might write that the day of the Crucifixion follows the arrest in the Garden of Gethsemane.
The Day of the Crucifixion
We know Jesus was crucified in the day time, for it is written that,
Now from the sixth hour there was darkness over all the land unto the ninth hour. (Matt 27:45)
According to the custom of the time, the time of day was measured from dawn, rather than as we do today from midnight. Therefore, this took place between high noon and 3pm in the afternoon.
We can capture this with the assumption that,
Finally, we know from the record that the next day was the Sabbath, primarily because those who buried Him had to press to get Him into the tomb before the Sabbath, lest His body remain on the cross all the next day.
And now when the even was come, because it was the preparation, that is, the day before the sabbath, Joseph of Arimathaea, an honourable counsellor, which also waited for the kingdom of God, came, and went in boldly unto Pilate, and craved the body of Jesus. And Pilate marvelled if he were already dead: and calling unto him the centurion, he asked him whether he had been any while dead. And when he knew it of the centurion, he gave the body to Joseph.
And he bought fine linen, and took him down, and wrapped him in the linen, and laid him in a sepulchre which was hewn out of a rock, and rolled a stone unto the door of the sepulchre. (Mark 15:42-46)
From this we might conclude not only that the crucifixion didn’t take place on a Sabbath,
but also that the day of the crucifixion was immediately followed by a Sabbath.
We also know from this description that, in the language of the time, the day prior to the Sabbath was called the “preparation day”. Let’s assume that this preparation day describes the daylight portion of the day as well.
We also know that the day following the preparation day is a Sabbath.
Likewise, no Sabbath shall take place unless it is preceded by a preparation day.
Note the extra requirement here that this criteria only applies to the daytime. Since the preparation day cannot take place at nighttime, based upon our assumption above, without this extra condition there could be no Sabbaths.
At one time I was going to declare the preparation day to be the day of the Crucifixion. I think I’ll just assert this instead, and so let the solver do the proof for me.
Finally, since there are things that happen after the crucifixion, let’s keep track of those in two ways. First, once the crucifixion has passed, then Jesus had been crucified. We can write this as,
We also know that He was only crucified once. While this might seem obvious to you and I, the formal tool does require this information.
Three Days and Three Nights
Perhaps the most controversial part of all of this is including the prophecy that Jesus was going to spend three days and three nights in the tomb.
For as Jonas was three days and three nights in the whale’s belly; so shall the Son of man be three days and three nights in the heart of the earth. (Matt 12:40)
So let’s count these out. First, He enters the tomb following the crucifixion, and then leaves it after three days and three nights.
The check is off by one from six, for the simple reason that we are reasoning about the next clock cycle, but more on that in a bit.
For now, let’s count the days,
and the nights when He is in the tomb.
We’ll know He was in the tomb for three days and three nights when these two counters equal three.
Now we can put our test together: If He’s been crucified, yet is no longer in the tomb, then He must’ve been in the tomb for three days and three nights:
This trace might therefore look like Fig. 3 below.
So, why did we transition on
5 instead of
6 above? Because we counted
as our first time-step. Hence,
5 are six steps. If you examine the
trace in Fig. 3 at the right, you can see that,
yes, we did count three days and three nights as desired, until He was out
of the tomb.
Yes, I’ve heard the arguments for fewer days. The problem is that if He was crucified on a Friday (the commonly proposed theory), then he would have been in the ground for one day and two nights, not three days and three nights. The answer I’ve been given, that the ancient Greeks didn’t know how to count properly just doesn’t hold water for me. The historical record tells us that people were counting days as early as the flood, and that by the time of Christ they knew how to calculate interest. So, I don’t buy the argument that the ancient Greeks didn’t know how to count.
Three days and three nights, therefore, must mean three days and three nights.
The Spices and the Soldiers
After Jesus was buried, certain women which came from Galilee went and prepared spices, and then rested.
And that day was the preparation, and the sabbath drew on. And the women also, which came with him from Galilee, followed after, and beheld the sepulchre, and how his body was laid. And they returned, and prepared spices and ointments; and rested the sabbath day according to the commandment. (Luke 23:54-56)
This tells us that these women were devout in their faith, and so they wouldn’t have prepared any spices on the sabbath. We can also draw from this that Jesus was in the tomb when they prepared the spices. We also know that, without artificial light, the spices would’ve been very difficult to prepare anything, so they didn’t do this at night. That leaves us with the following assumption:
Finally, in order to check whether, on the Resurrection day, these spices had been prepared or not, we’ll register a value to keep track that they had been prepared.
Now, while Jesus was in the tomb, the chief priests and Pharisees came to ask for a guard to be posted,
Now the next day, that followed the day of the preparation, the chief priests and Pharisees came together unto Pilate,
Saying, Sir, we remember that that deceiver said, while he was yet alive, After three days I will rise again. Command therefore that the sepulchre be made sure until the third day, lest his disciples come by night, and steal him away, and say unto the people, He is risen from the dead: so the last error shall be worse than the first. Pilate said unto them, Ye have a watch: go your way, make it as sure as ye can. So they went, and made the sepulchre sure, sealing the stone, and setting a watch. (Matt 27:62-66)
Note here that, again, the three day prophecy is confirmed–even by those who didn’t believe Him. But I digress.
While the following logic captures this idea of the day following the day of preparation, it is perhaps more complicated than it needs to be. The reason for the extra complication is that the “preparation day” was the day of the crucifixion, and the day after is not one time step later, but rather two.
Following this request, we know the tomb was guarded, as shown in Fig. 5 on the right.
Of course, this places the request on the Sabbath day. In many ways, I find it strange that the chief priests would go to Pilate on the Sabbath day, but perhaps it’s no stranger than the rest of their actions that week. For example, trying Jesus at night was already a violation of Jewish law. If the chief priests were willing to violate one law in such a gross manner, why should they be expected to hold to the rest of Jewish laws and customs?
Constraining the Resurrection
We’d also like to determine when Jesus was resurrected. Since this is one of those things we want to determine, we want to make absolute certain that it is only minimally constrained. One obvious constraint would be that He can’t be resurrected until He’s been crucified. I’m going to add one more, though: He can’t be resurrected unless He’s no longer in the tomb. Therefore,
I’ll go one step more, though, and add yet another constraint.
This one will pin down the exact time of the resurrection–to within the
structure of our timeline. Specifically, let’s define
as the first clock period when He’s no longer in the tomb. Hence,
This should be a sufficient constraint for the solver to match what we might expect.
This leaves us with one final set of constraints–the first day of the week when the women come to the tomb to find Him gone. This is well attested by every one of the Gospels.
In the end of the sabbath, as it began to dawn toward the first day of the week, came Mary Magdalene and the other Mary to see the sepulchre. (Matt 28:1)
And when the sabbath was past, Mary Magdalene, and Mary the mother of James, and Salome, had bought sweet spices, that they might come and anoint him. And very early in the morning the first day of the week, they came unto the sepulchre at the rising of the sun. (Mark 16:1-2)
Now upon the first day of the week, very early in the morning, they came unto the sepulchre, bringing the spices which they had prepared, and certain others with them. And they found the stone rolled away from the sepulchre. (Luke 24:1-2)
The first day of the week cometh Mary Magdalene early, when it was yet dark, unto the sepulchre, and seeth the stone taken away from the sepulchre. (John 20:1)
Hence, the morning visit to the tomb must have taken place on Sunday.
Why was the first day a Sunday, as opposed to any other day? Because, it is recorded in Exodus that,
Six days shalt thou labour, and do all thy work: But the seventh day is the sabbath of the LORD thy God: in it thou shalt not do any work, thou, nor thy son, nor thy daughter, thy manservant, nor thy maidservant, nor thy cattle, nor thy stranger that is within thy gates: For in six days the LORD made heaven and earth, the sea, and all that in them is, and rested the seventh day: wherefore the LORD blessed the sabbath day, and hallowed it. (Ex 20:9-11)
Ever since the commandment, and perhaps even before as well, the seventh day of the week has been maintained as the Jewish Sabbath. We know today that this seventh day is Saturday, therefore the “first day of the week” must be a Sunday.
This isn’t all of it either. We also know that when the women visited the tomb, they found it empty.
And, behold, there was a great earthquake: for the angel of the Lord descended from heaven, and came and rolled back the stone from the door, and sat upon it. His countenance was like lightning, and his raiment white as snow: And for fear of him the keepers did shake, and became as dead men.
And the angel answered and said unto the women, Fear not ye: for I know that ye seek Jesus, which was crucified. He is not here: for he is risen, as he said. Come, see the place where the Lord lay. And go quickly, and tell his disciples that he is risen from the dead; and, behold, he goeth before you into Galilee; there shall ye see him: lo, I have told you. (Matt 28:2-7)
And they said among themselves, Who shall roll us away the stone from the door of the sepulchre?
And when they looked, they saw that the stone was rolled away: for it was very great.
And entering into the sepulchre, they saw a young man sitting on the right side, clothed in a long white garment; and they were affrighted. And he saith unto them, Be not affrighted: Ye seek Jesus of Nazareth, which was crucified: he is risen; he is not here: behold the place where they laid him. (Mark 16:3-6)
And they found the stone rolled away from the sepulchre. And they entered in, and found not the body of the Lord Jesus.
And it came to pass, as they were much perplexed thereabout, behold, two men stood by them in shining garments: And as they were afraid, and bowed down their faces to the earth, they said unto them, Why seek ye the living among the dead? He is not here, but is risen: remember how he spake unto you when he was yet in Galilee, Saying, The Son of man must be delivered into the hands of sinful men, and be crucified, and the third day rise again.
And they remembered his words, And returned from the sepulchre, and told all these things unto the eleven, and to all the rest. (Luke 24:2-9)
So they ran both together: and the other disciple did outrun Peter, and came first to the sepulchre. And he stooping down, and looking in, saw the linen clothes lying; yet went he not in.
Then cometh Simon Peter following him, and went into the sepulchre, and seeth the linen clothes lie, And the napkin, that was about his head, not lying with the linen clothes, but wrapped together in a place by itself.
Then went in also that other disciple, which came first to the sepulchre, and he saw, and believed. (John 20:4-8)
At this point, what do we know from the accounts of these witnesses? We know that the tomb was empty, that the women had prepared spices, that they came to the tomb after dawn on a Sunday, and that the guards were still there.
The Resurrection: Putting it all together
So what do you get when you put all of this together?
Well first, if you don’t get your properties right, you’ll get a contradiction. Worse, since most of our properties are assumptions, the contradiction will end without a trace, you’ll simply see,
That doesn’t help.
However, if you bisect your assumptions, you’ll often find the problem. The properties discussed above have been checked, so there are no (more) contradictions within them. Indeed, you can check them out here if you would like. I’ve even posted the SymbiYosys script for reference.
Similarly, since we’re primarily running a cover proof, if the cover fails, you might wish to back up and cover all of the steps leading up to the final one. When you find the point that fails, you can again bisect the assumptions to find the one that is contradictory. (Yes, I needed to do this too, although I’ve since cleaned up these extraneous cover statements.)
As an example of a contradictory property, if you assume that the Crucifixion took place on a Friday, you would find no solution to these properties.
When you put it all together, you’ll get something like Fig. 6 below.
You’ll notice some very fascinating things about this figure that go contrary to popular belief.
Jesus wasn’t crucified on a Friday. A Friday crucifixion would’ve violated several properties of the Biblical account. First, no matter how you count it, a Friday crucifixion would not have left him in the ground for three days and three nights. Second, had He been crucified on a Friday, there would’ve been no time for the women to purchase and prepare their spices–something that cannot be done on the Sabbath day. Third, even the chief priests expected something to happen on the third day.
On the other hand, you might choose to find that this conclusion says a lot about me. For example, you might notice that I don’t much care what any church says or teaches about “Good Friday”–I care only about what the Bible teaches. As a result, I don’t suffer from any crisis of faith when I come across information that might contradict what the Bible teaches: I just choose to believe what the Bible says.
Incidentally, this is also the meaning of the word “epanorthosis” used in 2Tim 3:16, and translated as “correction”, when Paul uses it to describe the nature of God’s words:
All scripture is given by inspiration of God, and is profitable for doctrine, for reproof, for correction, for instruction in righteousness: (2Tim 3:16)
Indeed, the Greek Lexicon defines epanorthosis as: 1. Restoration to an upright or right state, 2. Correction, improvement of life or character.
In this case, we can correct our understanding of the Resurrection by simply paying attention to the Bible itself–as 2Tim 3:16 suggests.
Jesus wasn’t in the tomb when the angel rolled the stone away. Therefore the actual resurrection must have occurred beforehand.
This actually corresponds to the Gospel accounts: when the angel rolled the stone away, the women were invited to look into the tomb to verify that it was indeed and already empty.
But then how did He get out? Good question. Let me answer that by asking how He got into the upper room later that day:
Then the same day at evening, being the first day of the week, when the doors were shut where the disciples were assembled for fear of the Jews, came Jesus and stood in the midst, and saith unto them, Peace be unto you. (John 20:19)
Personally, I judge walking through walls to be easier than rising from the dead in the first place, so this theory of being able to walk through the tomb walls doesn’t really bother me.
There were two Sabbath days on crucifixion week.
Wait, what? Saturday is the Sabbath! How could there be two Sabbath days?!
As it turns out, Sabbath’s take place on more than just Saturdays. Consider this passage of Leviticus describing the Passover feast:
In the fourteenth day of the first month at even is the LORD’s passover. And on the fifteenth day of the same month is the feast of unleavened bread unto the LORD: seven days ye must eat unleavened bread. In the first day ye shall have an holy convocation: ye shall do no servile work therein. But ye shall offer an offering made by fire unto the LORD seven days: in the seventh day is an holy convocation: ye shall do no servile work therein. (Lev 23:5-8)
While I’m no expert in ancient Jewish customs, I will note that during this week of the Passover, there are two specific days where no work is to be done. These would be rest days, also known as Sabbaths. I would also note that no enduring calendar is based upon weeks, nor could it be, since as you and I both know there are 365 days in a year, which is just a touch longer than 52 weeks per year. Hence, in order to keep the year matching the seasons, the 14th day of the first month would by necessity need to wander through which day of the week it landed upon–forcing a Sabbath rest on days other than Saturday alone.
What conclusion should be drawn from this discussion of the Resurrection? First, that the Resurrection happened. Over 500 people saw and witnessed the resurrected Christ. Indeed, Christianity would make no sense if there was no Resurrection.
The second relevant point of the Resurrection follows Jesus’ explanation of its importance:
There was a certain rich man, which was clothed in purple and fine linen, and fared sumptuously every day: And there was a certain beggar named Lazarus, which was laid at his gate, full of sores, And desiring to be fed with the crumbs which fell from the rich man’s table: moreover the dogs came and licked his sores.
And it came to pass, that the beggar died, and was carried by the angels into Abraham’s bosom: the rich man also died, and was buried;
And in hell he lift up his eyes, being in torments, and seeth Abraham afar off, and Lazarus in his bosom. And he cried and said, Father Abraham, have mercy on me, and send Lazarus, that he may dip the tip of his finger in water, and cool my tongue; for I am tormented in this flame.
But Abraham said, Son, remember that thou in thy lifetime receivedst thy good things, and likewise Lazarus evil things: but now he is comforted, and thou art tormented. And beside all this, between us and you there is a great gulf fixed: so that they which would pass from hence to you cannot; neither can they pass to us, that would come from thence.
Then he said, I pray thee therefore, father, that thou wouldest send him to my father’s house: For I have five brethren; that he may testify unto them, lest they also come into this place of torment.
Abraham saith unto him, They have Moses and the prophets; let them hear them.
And he said, Nay, father Abraham: but if one went unto them from the dead, they will repent.
And he said unto him, If they hear not Moses and the prophets, neither will they be persuaded, though one rose from the dead. (Luke 16:19-31)
The rich man begged for someone to come back from the dead to warn of the torment waiting for those who have not believed. God was kind enough to grant the rich man’s wish. As a result, we can now say that someone has come back from the dead.
Tell me, was Abraham right? Or will you hear hear the words of Jesus today?
My third point is more personal: I know the Resurrection is true, because of the change that has taken place in my own life once I chose to trust the only Christ. I was once a sinner, a liar, thief, and worse. Once I chose to trust the Lord, He transformed my life and I am now no longer the wicked man I once was.
Hallelujah! Thank you, Lord Jesus, for changing my life.
This change could be yours as well, if you chose to trust Him as I have done. Will you hear his words today?
He is not here: for he is risen, as he said. Come, see the place where the Lord lay. (Matthew 28:6)